Theorem mpanr12 718

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  f1ofvswap  7306  2dom  9042  limensuci  9156  frinsg  9739  djuen  10229  isfin1-3  10445  prlem934  11099  0idsr  11163  1idsr  11164  00sr  11165  addresr  11204  mulresr  11205  reclt1  12193  crne0  12294  nominpos  12564  fvf1tp  13909  expnass  14332  faclbnd2  14415  crim  15262  01sqrexlem1  15389  01sqrexlem7  15395  sqrt00  15410  sqreulem  15507  mulcn2  15743  ege2le3  16236  sin02gt0  16340  opoe  16513  oddprm  16968  pythagtriplem2  16975  pythagtriplem3  16976  pythagtriplem16  16988  pythagtrip  16992  pc1  17013  prmlem0  17263  acsfn0  17814  mgpress  20350  abvneg  21063  matunitlindflem1  22974  pmatcollpw3  23082  leordtval2  23510  txswaphmeo  24104  iccntr  25121  dvlipcn  26294  sinq34lt0t  26820  cosordlem  26840  efif1olem3  26854  lgamgulmlem2  27339  basellem3  27392  ppiub  27513  bposlem9  27601  lgsne0  27644  lgsdinn0  27654  chebbnd1  27781  eupth2lem3lem4  30814  mayete3i  32312  lnop0  32550  nmcexi  32610  nmoptrii  32678  nmopcoadji  32685  hstle1  32810  hst0  32817  strlem5  32839  jplem1  32852  vonf1wev  35860  vonf1owevOLD  35862  subfacp1lem5  35918  limsucncmpi  37203  poimirlem15  38521  dvasin  38590  fdc  38647  eldioph3b  43729  oaabsb  44254  tfsconcatfv2  44300  omssaxinf2  45930  or2expropbi  48048  ich2exprop  48497  sprsymrelfolem2  48519  clnbgrisubgrgrim  48974  sinhpcosh  50777