Metamath Proof Explorer
		
		
		
		Description:  If a wff is true, it is true for at least one instance.  Deduction form
       of 19.8a .  (Contributed by DAW, 13-Feb-2017)
		
			
				
					|  |  | Ref | Expression | 
					
						|  | Hypothesis | 19.8ad.1 |  | 
				
					|  | Assertion | 19.8ad |  | 
			
		
		
			
				Proof
				
					
						| Step | Hyp | Ref | Expression | 
						
							| 1 |  | 19.8ad.1 |  | 
						
							| 2 |  | 19.8a |  | 
						
							| 3 | 1 2 | syl |  |