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  7306  2dom  9028  limensuci  9142  frinsg  9724  djuen  10154  isfin1-3  10371  prlem934  11019  0idsr  11083  1idsr  11084  00sr  11085  addresr  11124  mulresr  11125  reclt1  12111  crne0  12212  nominpos  12482  fvf1tp  13824  expnass  14246  faclbnd2  14329  crim  15168  01sqrexlem1  15295  01sqrexlem7  15301  sqrt00  15316  sqreulem  15413  mulcn2  15649  ege2le3  16145  sin02gt0  16249  opoe  16422  oddprm  16871  pythagtriplem2  16878  pythagtriplem3  16879  pythagtriplem16  16891  pythagtrip  16895  pc1  16916  prmlem0  17166  acsfn0  17717  mgpress  20227  abvneg  20910  pmatcollpw3  22922  leordtval2  23350  txswaphmeo  23943  iccntr  24960  dvlipcn  26134  sinq34lt0t  26655  cosordlem  26676  efif1olem3  26690  lgamgulmlem2  27175  basellem3  27228  ppiub  27349  bposlem9  27437  lgsne0  27480  lgsdinn0  27490  chebbnd1  27617  eupth2lem3lem4  30563  mayete3i  32061  lnop0  32299  nmcexi  32359  nmoptrii  32427  nmopcoadji  32434  hstle1  32559  hst0  32566  strlem5  32588  jplem1  32601  vonf1wev  35573  vonf1owevOLD  35575  subfacp1lem5  35657  limsucncmpi  36937  matunitlindflem1  38248  poimirlem15  38267  dvasin  38336  fdc  38377  eldioph3b  43479  oaabsb  44004  tfsconcatfv2  44050  omssaxinf2  45680  or2expropbi  47754  ich2exprop  48203  sprsymrelfolem2  48225  clnbgrisubgrgrim  48680  sinhpcosh  50501