Metamath Proof Explorer
		
		
		
		Description:  An inference based on modus ponens.  (Contributed by NM, 4-Dec-2006)
		
			
				
					|  |  | Ref | Expression | 
					
						|  | Hypotheses | mpd3an23.1 |  | 
					
						|  |  | mpd3an23.2 |  | 
					
						|  |  | mpd3an23.3 |  | 
				
					|  | Assertion | mpd3an23 |  | 
			
		
		
			
				Proof
				
					
						| Step | Hyp | Ref | Expression | 
						
							| 1 |  | mpd3an23.1 |  | 
						
							| 2 |  | mpd3an23.2 |  | 
						
							| 3 |  | mpd3an23.3 |  | 
						
							| 4 |  | id |  | 
						
							| 5 | 4 1 2 3 | syl3anc |  |