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  7261  2dom  8977  limensuci  9091  frinsg  9675  djuen  10092  isfin1-3  10308  prlem934  10956  0idsr  11020  1idsr  11021  00sr  11022  addresr  11061  mulresr  11062  reclt1  12051  crne0  12152  nominpos  12414  fvf1tp  13748  expnass  14170  faclbnd2  14253  crim  15077  01sqrexlem1  15204  01sqrexlem7  15210  sqrt00  15225  sqreulem  15322  mulcn2  15558  ege2le3  16055  sin02gt0  16159  opoe  16332  oddprm  16781  pythagtriplem2  16788  pythagtriplem3  16789  pythagtriplem16  16801  pythagtrip  16805  pc1  16826  prmlem0  17076  acsfn0  17626  mgpress  20131  abvneg  20803  pmatcollpw3  22749  leordtval2  23177  txswaphmeo  23770  iccntr  24787  dvlipcn  25961  sinq34lt0t  26473  cosordlem  26494  efif1olem3  26508  lgamgulmlem2  26993  basellem3  27046  ppiub  27167  bposlem9  27255  lgsne0  27298  lgsdinn0  27308  chebbnd1  27435  eupth2lem3lem4  30301  mayete3i  31799  lnop0  32037  nmcexi  32097  nmoptrii  32165  nmopcoadji  32172  hstle1  32297  hst0  32304  strlem5  32326  jplem1  32339  vonf1owev  35290  subfacp1lem5  35366  limsucncmpi  36627  matunitlindflem1  37937  poimirlem15  37956  dvasin  38025  fdc  38066  eldioph3b  43197  oaabsb  43722  tfsconcatfv2  43768  omssaxinf2  45415  or2expropbi  47482  ich2exprop  47931  sprsymrelfolem2  47953  clnbgrisubgrgrim  48408  sinhpcosh  50215