Metamath Proof Explorer
		
		
		
		Description:  Inference form of dfvd3an .  (Contributed by Alan Sare, 13-Jun-2015)
       (Proof modification is discouraged.)  (New usage is discouraged.)
		
			
				
					|  |  | Ref | Expression | 
					
						|  | Hypothesis | dfvd3ani.1 |  | 
				
					|  | Assertion | dfvd3ani |  | 
			
		
		
			
				Proof
				
					
						| Step | Hyp | Ref | Expression | 
						
							| 1 |  | dfvd3ani.1 |  | 
						
							| 2 |  | dfvd3an |  | 
						
							| 3 | 1 2 | mpbi |  |