MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpan2i Unicode version

Theorem mpan2i 677
Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
Hypotheses
Ref Expression
mpan2i.1
mpan2i.2
Assertion
Ref Expression
mpan2i

Proof of Theorem mpan2i
StepHypRef Expression
1 mpan2i.1 . . 3
21a1i 11 . 2
3 mpan2i.2 . 2
42, 3mpan2d 674 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  tcwf  8322  cflecard  8654  sqrlem7  13082  setciso  15418  lsmss1  16684  sincosq1lem  22890  pjcompi  26590  mdsl1i  27240  dfon2lem3  29217  dfon2lem7  29221  tan2h  30047  dvasin  30103  ismrc  30633  rngciso  32790  rngcisoOLD  32802  ringciso  32841  ringcisoOLD  32865  aacllem  33216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator