Theorem mpanr12 702

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  wfisgOLD  6257  f1ofvswap  7178  2dom  8820  limensuci  8940  phplem4OLD  9003  unfiOLD  9081  fiint  9091  frinsg  9509  djuen  9925  isfin1-3  10142  prlem934  10789  0idsr  10853  1idsr  10854  00sr  10855  addresr  10894  mulresr  10895  reclt1  11870  crne0  11966  nominpos  12210  expnass  13924  faclbnd2  14005  crim  14826  sqrlem1  14954  sqrlem7  14960  sqrt00  14975  sqreulem  15071  mulcn2  15305  ege2le3  15799  sin02gt0  15901  opoe  16072  oddprm  16511  pythagtriplem2  16518  pythagtriplem3  16519  pythagtriplem16  16531  pythagtrip  16535  pc1  16556  prmlem0  16807  acsfn0  17369  mgpress  19735  mgpressOLD  19736  abvneg  20094  pmatcollpw3  21933  leordtval2  22363  txswaphmeo  22956  iccntr  23984  dvlipcn  25158  sinq34lt0t  25666  cosordlem  25686  efif1olem3  25700  lgamgulmlem2  26179  basellem3  26232  ppiub  26352  bposlem9  26440  lgsne0  26483  lgsdinn0  26493  chebbnd1  26620  eupth2lem3lem4  28595  mayete3i  30090  lnop0  30328  nmcexi  30388  nmoptrii  30456  nmopcoadji  30463  hstle1  30588  hst0  30595  strlem5  30617  jplem1  30630  cnvoprabOLD  31055  subfacp1lem5  33146  limsucncmpi  34634  matunitlindflem1  35773  poimirlem15  35792  dvasin  35861  fdc  35903  eldioph3b  40587  or2expropbi  44528  ich2exprop  44923  sprsymrelfolem2  44945  sinhpcosh  46442