Theorem mpanl12 715

Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses

Ref	Expression
mpanl12.1	⊢ 𝜑
mpanl12.2	⊢ 𝜓
mpanl12.3	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mpanl12	⊢ (𝜒 → 𝜃)

Proof of Theorem mpanl12

Step	Hyp	Ref	Expression
1		mpanl12.2	. 2 ⊢ 𝜓
2		mpanl12.1	. . 3 ⊢ 𝜑
3		mpanl12.3	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	mpanl1 713	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 703	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:  spcimgfi1  3512  reuun1  4274  frminex  5630  tz6.26i  6344  wfii  6346  tfr2ALT  8393  tfr3ALT  8394  opthreg  9603  unsnen  10618  axcnre  11230  addgt0  11783  addgegt0  11784  addgtge0  11785  addge0  11786  addgt0i  11836  addge0i  11837  addgegt0i  11838  add20i  11840  mulge0i  11844  recextlem1  11927  recne0  11968  recdiv  12004  rec11i  12039  recgt1  12194  prodgt0i  12205  xadddi2  13408  iccshftri  13599  iccshftli  13601  iccdili  13603  icccntri  13605  mulexpz  14225  expaddz  14229  m1expeven  14232  iexpcyc  14331  cnpart  15387  resqrex  15397  sqreulem  15507  amgm2  15517  rlim  15642  ello12  15663  elo12  15674  bpolylem  16194  ege2le3  16236  dvdslelem  16459  divalglem1  16544  divalglem6  16548  divalglem9  16551  gcdaddmlem  16676  sqnprm  16858  prmlem1  17265  prmlem2  17278  m1expaddsub  19692  psgnuni  19693  gzrngunitlem  21718  lmres  23598  zdis  25116  iihalf1  25232  lmclimf  25605  vitali  25914  ismbf  25929  ismbfcn  25930  mbfconst  25934  cncombf  25959  cnmbf  25960  limcfval  26172  dvnfre  26252  quotlem  26603  ulmval  26689  ulmpm  26692  abelthlem2  26741  abelthlem3  26742  abelthlem5  26744  abelthlem7  26747  efcvx  26758  logtayl  26970  logccv  26973  cxpcn3  27058  emcllem2  27306  zetacvg  27324  basellem5  27394  bposlem7  27599  chebbnd1lem3  27780  dchrisumlem3  27800  iscgrgd  28958  axcontlem2  29525  nv1  31259  blocnilem  31388  ipasslem8  31421  siii  31437  ubthlem1  31454  norm1  31833  hhshsslem2  31852  hoscli  32346  hodcli  32347  cnlnadjlem7  32657  adjbdln  32667  pjnmopi  32732  strlem1  32834  rexdiv  33474  tpr2rico  34526  qqhre  34634  signsply0  35163  subfacval3  35923  erdszelem4  35928  erdszelem8  35932  elmrsubrn  36254  rdgprc  36526  fwddifval  36897  fwddifnval  36898  exrecfnlem  38270  poimirlem29  38535  ismblfin  38547  itg2addnclem  38557  caures  38662  sswfaxreg  45929  cjnpoly  47883  pgnbgreunbgrlem1  49155  pgnbgreunbgrlem4  49161  iooii  49970  icccldii  49971