Theorem mpanr12 703

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 701	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 689	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  6355  f1ofvswap  7306  2dom  9032  limensuci  9155  phplem4OLD  9222  unfiOLD  9315  fiint  9326  frinsg  9748  djuen  10166  isfin1-3  10383  prlem934  11030  0idsr  11094  1idsr  11095  00sr  11096  addresr  11135  mulresr  11136  reclt1  12113  crne0  12209  nominpos  12453  expnass  14176  faclbnd2  14255  crim  15066  01sqrexlem1  15193  01sqrexlem7  15199  sqrt00  15214  sqreulem  15310  mulcn2  15544  ege2le3  16037  sin02gt0  16139  opoe  16310  oddprm  16747  pythagtriplem2  16754  pythagtriplem3  16755  pythagtriplem16  16767  pythagtrip  16771  pc1  16792  prmlem0  17043  acsfn0  17608  mgpress  20043  mgpressOLD  20044  abvneg  20585  pmatcollpw3  22506  leordtval2  22936  txswaphmeo  23529  iccntr  24557  dvlipcn  25735  sinq34lt0t  26243  cosordlem  26263  efif1olem3  26277  lgamgulmlem2  26758  basellem3  26811  ppiub  26931  bposlem9  27019  lgsne0  27062  lgsdinn0  27072  chebbnd1  27199  eupth2lem3lem4  29739  mayete3i  31236  lnop0  31474  nmcexi  31534  nmoptrii  31602  nmopcoadji  31609  hstle1  31734  hst0  31741  strlem5  31763  jplem1  31776  cnvoprabOLD  32200  subfacp1lem5  34461  limsucncmpi  35633  matunitlindflem1  36787  poimirlem15  36806  dvasin  36875  fdc  36916  eldioph3b  41805  oaabsb  42346  tfsconcatfv2  42392  or2expropbi  46043  ich2exprop  46438  sprsymrelfolem2  46460  sinhpcosh  47873