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  7284  2dom  9004  limensuci  9123  fiintOLD  9285  frinsg  9711  djuen  10130  isfin1-3  10346  prlem934  10993  0idsr  11057  1idsr  11058  00sr  11059  addresr  11098  mulresr  11099  reclt1  12085  crne0  12186  nominpos  12426  fvf1tp  13758  expnass  14180  faclbnd2  14263  crim  15088  01sqrexlem1  15215  01sqrexlem7  15221  sqrt00  15236  sqreulem  15333  mulcn2  15569  ege2le3  16063  sin02gt0  16167  opoe  16340  oddprm  16788  pythagtriplem2  16795  pythagtriplem3  16796  pythagtriplem16  16808  pythagtrip  16812  pc1  16833  prmlem0  17083  acsfn0  17628  mgpress  20066  abvneg  20742  pmatcollpw3  22678  leordtval2  23106  txswaphmeo  23699  iccntr  24717  dvlipcn  25906  sinq34lt0t  26425  cosordlem  26446  efif1olem3  26460  lgamgulmlem2  26947  basellem3  27000  ppiub  27122  bposlem9  27210  lgsne0  27253  lgsdinn0  27263  chebbnd1  27390  eupth2lem3lem4  30167  mayete3i  31664  lnop0  31902  nmcexi  31962  nmoptrii  32030  nmopcoadji  32037  hstle1  32162  hst0  32169  strlem5  32191  jplem1  32204  vonf1owev  35102  subfacp1lem5  35178  limsucncmpi  36440  matunitlindflem1  37617  poimirlem15  37636  dvasin  37705  fdc  37746  eldioph3b  42760  oaabsb  43290  tfsconcatfv2  43336  omssaxinf2  44985  or2expropbi  47039  ich2exprop  47476  sprsymrelfolem2  47498  clnbgrisubgrgrim  47936  sinhpcosh  49733