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  3514  reuun1  4277  frminex  5638  tz6.26i  6350  wfii  6352  tfr2ALT  8394  tfr3ALT  8395  opthreg  9601  unsnen  10565  axcnre  11177  addgt0  11728  addgegt0  11729  addgtge0  11730  addge0  11731  addgt0i  11781  addge0i  11782  addgegt0i  11783  add20i  11785  mulge0i  11789  recextlem1  11872  recne0  11913  recdiv  11949  rec11i  11984  recgt1  12139  prodgt0i  12150  xadddi2  13353  iccshftri  13544  iccshftli  13546  iccdili  13548  icccntri  13550  mulexpz  14170  expaddz  14174  m1expeven  14177  iexpcyc  14275  cnpart  15331  resqrex  15341  sqreulem  15451  amgm2  15461  rlim  15586  ello12  15607  elo12  15618  bpolylem  16140  ege2le3  16182  dvdslelem  16405  divalglem1  16490  divalglem6  16494  divalglem9  16497  gcdaddmlem  16620  sqnprm  16799  prmlem1  17205  prmlem2  17218  m1expaddsub  19631  psgnuni  19632  gzrngunitlem  21651  lmres  23531  zdis  25049  iihalf1  25165  lmclimf  25538  vitali  25847  ismbf  25862  ismbfcn  25863  mbfconst  25867  cncombf  25892  cnmbf  25893  limcfval  26106  dvnfre  26186  quotlem  26537  ulmval  26623  ulmpm  26626  abelthlem2  26675  abelthlem3  26676  abelthlem5  26678  abelthlem7  26681  efcvx  26692  logtayl  26905  logccv  26908  cxpcn3  26993  emcllem2  27241  zetacvg  27259  basellem5  27329  bposlem7  27534  chebbnd1lem3  27715  dchrisumlem3  27735  iscgrgd  28863  axcontlem2  29430  nv1  31164  blocnilem  31293  ipasslem8  31326  siii  31342  ubthlem1  31359  norm1  31738  hhshsslem2  31757  hoscli  32251  hodcli  32252  cnlnadjlem7  32562  adjbdln  32572  pjnmopi  32637  strlem1  32739  rexdiv  33379  tpr2rico  34430  qqhre  34538  signsply0  35067  subfacval3  35776  erdszelem4  35781  erdszelem8  35785  elmrsubrn  36107  rdgprc  36379  fwddifval  36750  fwddifnval  36751  exrecfnlem  38141  poimirlem29  38406  ismblfin  38418  itg2addnclem  38428  caures  38518  sswfaxreg  45818  cjnpoly  47765  pgnbgreunbgrlem1  49037  pgnbgreunbgrlem4  49043  iooii  49852  icccldii  49853