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  7240  2dom  8952  limensuci  9066  frinsg  9644  djuen  10061  isfin1-3  10277  prlem934  10924  0idsr  10988  1idsr  10989  00sr  10990  addresr  11029  mulresr  11030  reclt1  12017  crne0  12118  nominpos  12358  fvf1tp  13693  expnass  14115  faclbnd2  14198  crim  15022  01sqrexlem1  15149  01sqrexlem7  15155  sqrt00  15170  sqreulem  15267  mulcn2  15503  ege2le3  15997  sin02gt0  16101  opoe  16274  oddprm  16722  pythagtriplem2  16729  pythagtriplem3  16730  pythagtriplem16  16742  pythagtrip  16746  pc1  16767  prmlem0  17017  acsfn0  17566  mgpress  20069  abvneg  20742  pmatcollpw3  22700  leordtval2  23128  txswaphmeo  23721  iccntr  24738  dvlipcn  25927  sinq34lt0t  26446  cosordlem  26467  efif1olem3  26481  lgamgulmlem2  26968  basellem3  27021  ppiub  27143  bposlem9  27231  lgsne0  27274  lgsdinn0  27284  chebbnd1  27411  eupth2lem3lem4  30209  mayete3i  31706  lnop0  31944  nmcexi  32004  nmoptrii  32072  nmopcoadji  32079  hstle1  32204  hst0  32211  strlem5  32233  jplem1  32246  vonf1owev  35150  subfacp1lem5  35226  limsucncmpi  36485  matunitlindflem1  37662  poimirlem15  37681  dvasin  37750  fdc  37791  eldioph3b  42804  oaabsb  43333  tfsconcatfv2  43379  omssaxinf2  45027  or2expropbi  47071  ich2exprop  47508  sprsymrelfolem2  47530  clnbgrisubgrgrim  47969  sinhpcosh  49778