Theorem mpanr12 718

Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)

Hypotheses

Ref	Expression
mpanr12.1	⊢ 𝜓
mpanr12.2	⊢ 𝜒
mpanr12.3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
mpanr12	⊢ (𝜑 → 𝜃)

Proof of Theorem mpanr12

Step	Hyp	Ref	Expression
1		mpanr12.2	. 2 ⊢ 𝜒
2		mpanr12.1	. . 3 ⊢ 𝜓
3		mpanr12.3	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	mpanr1 716	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 704	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  f1ofvswap  7340  2dom  9089  limensuci  9203  frinsg  9785  djuen  10278  isfin1-3  10494  prlem934  11148  0idsr  11212  1idsr  11213  00sr  11214  addresr  11253  mulresr  11254  reclt1  12242  crne0  12343  nominpos  12613  fvf1tp  13959  expnass  14382  faclbnd2  14465  crim  15314  01sqrexlem1  15441  01sqrexlem7  15447  sqrt00  15462  sqreulem  15559  mulcn2  15795  ege2le3  16288  sin02gt0  16392  opoe  16565  oddprm  17020  pythagtriplem2  17027  pythagtriplem3  17028  pythagtriplem16  17040  pythagtrip  17044  pc1  17065  prmlem0  17315  acsfn0  17866  mgpress  20403  abvneg  21116  matunitlindflem1  23027  pmatcollpw3  23135  leordtval2  23563  txswaphmeo  24157  iccntr  25174  dvlipcn  26347  sinq34lt0t  26871  cosordlem  26891  efif1olem3  26905  lgamgulmlem2  27390  basellem3  27443  ppiub  27564  bposlem9  27652  lgsne0  27695  lgsdinn0  27705  chebbnd1  27832  eupth2lem3lem4  30865  mayete3i  32363  lnop0  32601  nmcexi  32661  nmoptrii  32729  nmopcoadji  32736  hstle1  32861  hst0  32868  strlem5  32890  jplem1  32903  vonf1wev  36049  vonf1owevOLD  36051  subfacp1lem5  36129  limsucncmpi  37424  poimirlem15  38758  dvasin  38827  fdc  38882  eldioph3b  43980  oaabsb  44499  tfsconcatfv2  44545  omssaxinf2  46184  or2expropbi  48319  ich2exprop  48768  sprsymrelfolem2  48790  clnbgrisubgrgrim  49245  sinhpcosh  51122