Theorem mpanr12 705

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 703	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 691	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  7283  2dom  9003  limensuci  9122  fiintOLD  9284  frinsg  9710  djuen  10129  isfin1-3  10345  prlem934  10992  0idsr  11056  1idsr  11057  00sr  11058  addresr  11097  mulresr  11098  reclt1  12084  crne0  12180  nominpos  12425  fvf1tp  13757  expnass  14179  faclbnd2  14262  crim  15087  01sqrexlem1  15214  01sqrexlem7  15220  sqrt00  15235  sqreulem  15332  mulcn2  15568  ege2le3  16062  sin02gt0  16166  opoe  16339  oddprm  16787  pythagtriplem2  16794  pythagtriplem3  16795  pythagtriplem16  16807  pythagtrip  16811  pc1  16832  prmlem0  17082  acsfn0  17627  mgpress  20065  abvneg  20741  pmatcollpw3  22677  leordtval2  23105  txswaphmeo  23698  iccntr  24716  dvlipcn  25905  sinq34lt0t  26424  cosordlem  26445  efif1olem3  26459  lgamgulmlem2  26946  basellem3  26999  ppiub  27121  bposlem9  27209  lgsne0  27252  lgsdinn0  27262  chebbnd1  27389  eupth2lem3lem4  30166  mayete3i  31663  lnop0  31901  nmcexi  31961  nmoptrii  32029  nmopcoadji  32036  hstle1  32161  hst0  32168  strlem5  32190  jplem1  32203  subfacp1lem5  35171  limsucncmpi  36428  matunitlindflem1  37605  poimirlem15  37624  dvasin  37693  fdc  37734  eldioph3b  42746  oaabsb  43276  tfsconcatfv2  43322  omssaxinf2  44971  or2expropbi  47025  ich2exprop  47462  sprsymrelfolem2  47484  clnbgrisubgrgrim  47922  sinhpcosh  49719