Theorem mpanr12 711

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 709	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 697	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 208  df-an 397

This theorem is referenced by:  f1ofvswap  7257  2dom  8974  limensuci  9088  frinsg  9673  djuen  10090  isfin1-3  10306  prlem934  10954  0idsr  11018  1idsr  11019  00sr  11020  addresr  11059  mulresr  11060  reclt1  12049  crne0  12150  nominpos  12412  fvf1tp  13746  expnass  14168  faclbnd2  14251  crim  15075  01sqrexlem1  15202  01sqrexlem7  15208  sqrt00  15223  sqreulem  15320  mulcn2  15556  ege2le3  16053  sin02gt0  16157  opoe  16330  oddprm  16779  pythagtriplem2  16786  pythagtriplem3  16787  pythagtriplem16  16799  pythagtrip  16803  pc1  16824  prmlem0  17074  acsfn0  17624  mgpress  20129  abvneg  20805  pmatcollpw3  22774  leordtval2  23202  txswaphmeo  23795  iccntr  24812  dvlipcn  25986  sinq34lt0t  26498  cosordlem  26519  efif1olem3  26533  lgamgulmlem2  27018  basellem3  27071  ppiub  27192  bposlem9  27280  lgsne0  27323  lgsdinn0  27333  chebbnd1  27460  eupth2lem3lem4  30326  mayete3i  31824  lnop0  32062  nmcexi  32122  nmoptrii  32190  nmopcoadji  32197  hstle1  32322  hst0  32329  strlem5  32351  jplem1  32364  vonf1owev  35343  subfacp1lem5  35419  limsucncmpi  36680  matunitlindflem1  37990  poimirlem15  38009  dvasin  38078  fdc  38119  eldioph3b  43221  oaabsb  43746  tfsconcatfv2  43792  omssaxinf2  45439  or2expropbi  47504  ich2exprop  47953  sprsymrelfolem2  47975  clnbgrisubgrgrim  48430  sinhpcosh  50237