Theorem mpanr12 704

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  wfisgOLD  6352  f1ofvswap  7299  2dom  9026  limensuci  9149  phplem4OLD  9216  unfiOLD  9309  fiint  9320  frinsg  9742  djuen  10160  isfin1-3  10377  prlem934  11024  0idsr  11088  1idsr  11089  00sr  11090  addresr  11129  mulresr  11130  reclt1  12105  crne0  12201  nominpos  12445  expnass  14168  faclbnd2  14247  crim  15058  01sqrexlem1  15185  01sqrexlem7  15191  sqrt00  15206  sqreulem  15302  mulcn2  15536  ege2le3  16029  sin02gt0  16131  opoe  16302  oddprm  16739  pythagtriplem2  16746  pythagtriplem3  16747  pythagtriplem16  16759  pythagtrip  16763  pc1  16784  prmlem0  17035  acsfn0  17600  mgpress  19994  mgpressOLD  19995  abvneg  20430  pmatcollpw3  22268  leordtval2  22698  txswaphmeo  23291  iccntr  24319  dvlipcn  25493  sinq34lt0t  26001  cosordlem  26021  efif1olem3  26035  lgamgulmlem2  26514  basellem3  26567  ppiub  26687  bposlem9  26775  lgsne0  26818  lgsdinn0  26828  chebbnd1  26955  eupth2lem3lem4  29464  mayete3i  30959  lnop0  31197  nmcexi  31257  nmoptrii  31325  nmopcoadji  31332  hstle1  31457  hst0  31464  strlem5  31486  jplem1  31499  cnvoprabOLD  31923  subfacp1lem5  34113  limsucncmpi  35268  matunitlindflem1  36422  poimirlem15  36441  dvasin  36510  fdc  36551  eldioph3b  41436  oaabsb  41977  tfsconcatfv2  42023  or2expropbi  45679  ich2exprop  46074  sprsymrelfolem2  46096  sinhpcosh  47687