Theorem mpanr12 715

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 713	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 701	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  f1ofvswap  7284  2dom  9004  limensuci  9118  frinsg  9702  djuen  10119  isfin1-3  10336  prlem934  10984  0idsr  11048  1idsr  11049  00sr  11050  addresr  11089  mulresr  11090  reclt1  12080  crne0  12181  nominpos  12451  fvf1tp  13792  expnass  14214  faclbnd2  14297  crim  15132  01sqrexlem1  15259  01sqrexlem7  15265  sqrt00  15280  sqreulem  15377  mulcn2  15613  ege2le3  16110  sin02gt0  16214  opoe  16387  oddprm  16836  pythagtriplem2  16843  pythagtriplem3  16844  pythagtriplem16  16856  pythagtrip  16860  pc1  16881  prmlem0  17131  acsfn0  17682  mgpress  20186  abvneg  20862  pmatcollpw3  22831  leordtval2  23259  txswaphmeo  23852  iccntr  24869  dvlipcn  26043  sinq34lt0t  26561  cosordlem  26582  efif1olem3  26596  lgamgulmlem2  27081  basellem3  27134  ppiub  27255  bposlem9  27343  lgsne0  27386  lgsdinn0  27396  chebbnd1  27523  eupth2lem3lem4  30389  mayete3i  31887  lnop0  32125  nmcexi  32185  nmoptrii  32253  nmopcoadji  32260  hstle1  32385  hst0  32392  strlem5  32414  jplem1  32427  vonf1wev  35411  vonf1owevOLD  35413  subfacp1lem5  35494  limsucncmpi  36765  matunitlindflem1  38075  poimirlem15  38094  dvasin  38163  fdc  38204  eldioph3b  43306  oaabsb  43831  tfsconcatfv2  43877  omssaxinf2  45524  or2expropbi  47588  ich2exprop  48037  sprsymrelfolem2  48059  clnbgrisubgrgrim  48514  sinhpcosh  50321