Theorem mpanr12 717

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  f1ofvswap  7294  2dom  9015  limensuci  9129  frinsg  9711  djuen  10141  isfin1-3  10358  prlem934  11006  0idsr  11070  1idsr  11071  00sr  11072  addresr  11111  mulresr  11112  reclt1  12098  crne0  12199  nominpos  12469  fvf1tp  13810  expnass  14232  faclbnd2  14315  crim  15154  01sqrexlem1  15281  01sqrexlem7  15287  sqrt00  15302  sqreulem  15399  mulcn2  15635  ege2le3  16132  sin02gt0  16236  opoe  16409  oddprm  16858  pythagtriplem2  16865  pythagtriplem3  16866  pythagtriplem16  16878  pythagtrip  16882  pc1  16903  prmlem0  17153  acsfn0  17704  mgpress  20214  abvneg  20895  pmatcollpw3  22898  leordtval2  23326  txswaphmeo  23919  iccntr  24936  dvlipcn  26110  sinq34lt0t  26628  cosordlem  26649  efif1olem3  26663  lgamgulmlem2  27148  basellem3  27201  ppiub  27322  bposlem9  27410  lgsne0  27453  lgsdinn0  27463  chebbnd1  27590  eupth2lem3lem4  30487  mayete3i  31985  lnop0  32223  nmcexi  32283  nmoptrii  32351  nmopcoadji  32358  hstle1  32483  hst0  32490  strlem5  32512  jplem1  32525  vonf1wev  35458  vonf1owevOLD  35460  subfacp1lem5  35542  limsucncmpi  36813  matunitlindflem1  38122  poimirlem15  38141  dvasin  38210  fdc  38251  eldioph3b  43353  oaabsb  43878  tfsconcatfv2  43924  omssaxinf2  45556  or2expropbi  47627  ich2exprop  48076  sprsymrelfolem2  48098  clnbgrisubgrgrim  48553  sinhpcosh  50370