Theorem mpanr12 706

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  f1ofvswap  7262  2dom  8979  limensuci  9093  frinsg  9675  djuen  10092  isfin1-3  10308  prlem934  10956  0idsr  11020  1idsr  11021  00sr  11022  addresr  11061  mulresr  11062  reclt1  12049  crne0  12150  nominpos  12390  fvf1tp  13721  expnass  14143  faclbnd2  14226  crim  15050  01sqrexlem1  15177  01sqrexlem7  15183  sqrt00  15198  sqreulem  15295  mulcn2  15531  ege2le3  16025  sin02gt0  16129  opoe  16302  oddprm  16750  pythagtriplem2  16757  pythagtriplem3  16758  pythagtriplem16  16770  pythagtrip  16774  pc1  16795  prmlem0  17045  acsfn0  17595  mgpress  20097  abvneg  20771  pmatcollpw3  22740  leordtval2  23168  txswaphmeo  23761  iccntr  24778  dvlipcn  25967  sinq34lt0t  26486  cosordlem  26507  efif1olem3  26521  lgamgulmlem2  27008  basellem3  27061  ppiub  27183  bposlem9  27271  lgsne0  27314  lgsdinn0  27324  chebbnd1  27451  eupth2lem3lem4  30318  mayete3i  31815  lnop0  32053  nmcexi  32113  nmoptrii  32181  nmopcoadji  32188  hstle1  32313  hst0  32320  strlem5  32342  jplem1  32355  vonf1owev  35321  subfacp1lem5  35397  limsucncmpi  36658  matunitlindflem1  37864  poimirlem15  37883  dvasin  37952  fdc  37993  eldioph3b  43119  oaabsb  43648  tfsconcatfv2  43694  omssaxinf2  45341  or2expropbi  47391  ich2exprop  47828  sprsymrelfolem2  47850  clnbgrisubgrgrim  48289  sinhpcosh  50096