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  7311  2dom  9041  limensuci  9155  frinsg  9737  djuen  10176  isfin1-3  10392  prlem934  11046  0idsr  11110  1idsr  11111  00sr  11112  addresr  11151  mulresr  11152  reclt1  12138  crne0  12239  nominpos  12509  fvf1tp  13854  expnass  14276  faclbnd2  14359  crim  15206  01sqrexlem1  15333  01sqrexlem7  15339  sqrt00  15354  sqreulem  15451  mulcn2  15687  ege2le3  16182  sin02gt0  16286  opoe  16459  oddprm  16908  pythagtriplem2  16915  pythagtriplem3  16916  pythagtriplem16  16928  pythagtrip  16932  pc1  16953  prmlem0  17203  acsfn0  17754  mgpress  20289  abvneg  20998  matunitlindflem1  22907  pmatcollpw3  23015  leordtval2  23443  txswaphmeo  24037  iccntr  25054  dvlipcn  26228  sinq34lt0t  26754  cosordlem  26775  efif1olem3  26789  lgamgulmlem2  27274  basellem3  27327  ppiub  27448  bposlem9  27536  lgsne0  27579  lgsdinn0  27589  chebbnd1  27716  eupth2lem3lem4  30719  mayete3i  32217  lnop0  32455  nmcexi  32515  nmoptrii  32583  nmopcoadji  32590  hstle1  32715  hst0  32722  strlem5  32744  jplem1  32757  vonf1wev  35713  vonf1owevOLD  35715  subfacp1lem5  35771  limsucncmpi  37072  poimirlem15  38392  dvasin  38461  fdc  38503  eldioph3b  43618  oaabsb  44143  tfsconcatfv2  44189  omssaxinf2  45819  or2expropbi  47930  ich2exprop  48379  sprsymrelfolem2  48401  clnbgrisubgrgrim  48856  sinhpcosh  50674