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  6356  f1ofvswap  7304  2dom  9030  limensuci  9153  phplem4OLD  9220  unfiOLD  9313  fiint  9324  frinsg  9746  djuen  10164  isfin1-3  10381  prlem934  11028  0idsr  11092  1idsr  11093  00sr  11094  addresr  11133  mulresr  11134  reclt1  12109  crne0  12205  nominpos  12449  expnass  14172  faclbnd2  14251  crim  15062  01sqrexlem1  15189  01sqrexlem7  15195  sqrt00  15210  sqreulem  15306  mulcn2  15540  ege2le3  16033  sin02gt0  16135  opoe  16306  oddprm  16743  pythagtriplem2  16750  pythagtriplem3  16751  pythagtriplem16  16763  pythagtrip  16767  pc1  16788  prmlem0  17039  acsfn0  17604  mgpress  20002  mgpressOLD  20003  abvneg  20442  pmatcollpw3  22286  leordtval2  22716  txswaphmeo  23309  iccntr  24337  dvlipcn  25511  sinq34lt0t  26019  cosordlem  26039  efif1olem3  26053  lgamgulmlem2  26534  basellem3  26587  ppiub  26707  bposlem9  26795  lgsne0  26838  lgsdinn0  26848  chebbnd1  26975  eupth2lem3lem4  29484  mayete3i  30981  lnop0  31219  nmcexi  31279  nmoptrii  31347  nmopcoadji  31354  hstle1  31479  hst0  31486  strlem5  31508  jplem1  31521  cnvoprabOLD  31945  subfacp1lem5  34175  limsucncmpi  35330  matunitlindflem1  36484  poimirlem15  36503  dvasin  36572  fdc  36613  eldioph3b  41503  oaabsb  42044  tfsconcatfv2  42090  or2expropbi  45744  ich2exprop  46139  sprsymrelfolem2  46161  sinhpcosh  47785