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  7315  2dom  9062  limensuci  9176  frinsg  9759  djuen  10252  isfin1-3  10468  prlem934  11122  0idsr  11186  1idsr  11187  00sr  11188  addresr  11227  mulresr  11228  reclt1  12216  crne0  12317  nominpos  12587  fvf1tp  13933  expnass  14356  faclbnd2  14439  crim  15288  01sqrexlem1  15415  01sqrexlem7  15421  sqrt00  15436  sqreulem  15533  mulcn2  15769  ege2le3  16262  sin02gt0  16366  opoe  16539  oddprm  16994  pythagtriplem2  17001  pythagtriplem3  17002  pythagtriplem16  17014  pythagtrip  17018  pc1  17039  prmlem0  17289  acsfn0  17840  mgpress  20376  abvneg  21089  matunitlindflem1  23000  pmatcollpw3  23108  leordtval2  23536  txswaphmeo  24130  iccntr  25147  dvlipcn  26320  sinq34lt0t  26844  cosordlem  26864  efif1olem3  26878  lgamgulmlem2  27363  basellem3  27416  ppiub  27537  bposlem9  27625  lgsne0  27668  lgsdinn0  27678  chebbnd1  27805  eupth2lem3lem4  30838  mayete3i  32336  lnop0  32574  nmcexi  32634  nmoptrii  32702  nmopcoadji  32709  hstle1  32834  hst0  32841  strlem5  32863  jplem1  32876  vonf1wev  35956  vonf1owevOLD  35958  subfacp1lem5  36036  limsucncmpi  37326  poimirlem15  38647  dvasin  38716  fdc  38773  eldioph3b  43870  oaabsb  44390  tfsconcatfv2  44436  omssaxinf2  46072  or2expropbi  48198  ich2exprop  48647  sprsymrelfolem2  48669  clnbgrisubgrgrim  49124  sinhpcosh  51002