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  9037  limensuci  9151  frinsg  9733  djuen  10172  isfin1-3  10388  prlem934  11036  0idsr  11100  1idsr  11101  00sr  11102  addresr  11141  mulresr  11142  reclt1  12128  crne0  12229  nominpos  12499  fvf1tp  13842  expnass  14264  faclbnd2  14347  crim  15192  01sqrexlem1  15319  01sqrexlem7  15325  sqrt00  15340  sqreulem  15437  mulcn2  15673  ege2le3  16169  sin02gt0  16273  opoe  16446  oddprm  16895  pythagtriplem2  16902  pythagtriplem3  16903  pythagtriplem16  16915  pythagtrip  16919  pc1  16940  prmlem0  17190  acsfn0  17741  mgpress  20257  abvneg  20966  pmatcollpw3  22978  leordtval2  23406  txswaphmeo  23999  iccntr  25016  dvlipcn  26190  sinq34lt0t  26711  cosordlem  26732  efif1olem3  26746  lgamgulmlem2  27231  basellem3  27284  ppiub  27405  bposlem9  27493  lgsne0  27536  lgsdinn0  27546  chebbnd1  27673  eupth2lem3lem4  30619  mayete3i  32117  lnop0  32355  nmcexi  32415  nmoptrii  32483  nmopcoadji  32490  hstle1  32615  hst0  32622  strlem5  32644  jplem1  32657  vonf1wev  35616  vonf1owevOLD  35618  subfacp1lem5  35697  limsucncmpi  36997  matunitlindflem1  38308  poimirlem15  38327  dvasin  38396  fdc  38437  eldioph3b  43537  oaabsb  44062  tfsconcatfv2  44108  omssaxinf2  45738  or2expropbi  47812  ich2exprop  48261  sprsymrelfolem2  48283  clnbgrisubgrgrim  48738  sinhpcosh  50559