Theorem mpanl12 703

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 701	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 691	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  spcimgfi1  3493  reuun1  4269  frminex  5611  tz6.26i  6314  wfii  6316  tfr2ALT  8342  tfr3ALT  8343  opthreg  9541  unsnen  10477  axcnre  11089  addgt0  11638  addgegt0  11639  addgtge0  11640  addge0  11641  addgt0i  11691  addge0i  11692  addgegt0i  11693  add20i  11695  mulge0i  11699  recextlem1  11782  recne0  11824  recdiv  11863  rec11i  11898  recgt1  12054  prodgt0i  12065  xadddi2  13251  iccshftri  13442  iccshftli  13444  iccdili  13446  icccntri  13448  mulexpz  14066  expaddz  14070  m1expeven  14073  iexpcyc  14171  cnpart  15204  resqrex  15214  sqreulem  15324  amgm2  15334  rlim  15459  ello12  15480  elo12  15491  bpolylem  16015  ege2le3  16057  dvdslelem  16280  divalglem1  16365  divalglem6  16369  divalglem9  16372  gcdaddmlem  16495  sqnprm  16674  prmlem1  17080  prmlem2  17092  m1expaddsub  19475  psgnuni  19476  gzrngunitlem  21414  lmres  23267  zdis  24784  iihalf1  24900  lmclimf  25273  vitali  25582  ismbf  25597  ismbfcn  25598  mbfconst  25602  cncombf  25627  cnmbf  25628  limcfval  25841  dvnfre  25921  quotlem  26268  ulmval  26347  ulmpm  26350  abelthlem2  26399  abelthlem3  26400  abelthlem5  26402  abelthlem7  26405  efcvx  26416  logtayl  26626  logccv  26629  cxpcn3  26714  emcllem2  26962  zetacvg  26980  basellem5  27050  bposlem7  27255  chebbnd1lem3  27436  dchrisumlem3  27456  iscgrgd  28583  axcontlem2  29036  nv1  30748  blocnilem  30877  ipasslem8  30910  siii  30926  ubthlem1  30943  norm1  31322  hhshsslem2  31341  hoscli  31835  hodcli  31836  cnlnadjlem7  32146  adjbdln  32156  pjnmopi  32221  strlem1  32323  rexdiv  32987  tpr2rico  34058  qqhre  34166  signsply0  34697  subfacval3  35373  erdszelem4  35378  erdszelem8  35382  elmrsubrn  35704  rdgprc  35976  fwddifval  36346  fwddifnval  36347  exrecfnlem  37697  poimirlem29  37972  ismblfin  37984  itg2addnclem  37994  caures  38083  sswfaxreg  45416  nthrucw  47318  cjnpoly  47339  pgnbgreunbgrlem1  48591  pgnbgreunbgrlem4  48597  iooii  49395  icccldii  49396