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  3492  reuun1  4268  frminex  5610  tz6.26i  6312  wfii  6314  tfr2ALT  8340  tfr3ALT  8341  opthreg  9539  unsnen  10475  axcnre  11087  addgt0  11636  addgegt0  11637  addgtge0  11638  addge0  11639  addgt0i  11689  addge0i  11690  addgegt0i  11691  add20i  11693  mulge0i  11697  recextlem1  11780  recne0  11822  recdiv  11861  rec11i  11896  recgt1  12052  prodgt0i  12063  xadddi2  13249  iccshftri  13440  iccshftli  13442  iccdili  13444  icccntri  13446  mulexpz  14064  expaddz  14068  m1expeven  14071  iexpcyc  14169  cnpart  15202  resqrex  15212  sqreulem  15322  amgm2  15332  rlim  15457  ello12  15478  elo12  15489  bpolylem  16013  ege2le3  16055  dvdslelem  16278  divalglem1  16363  divalglem6  16367  divalglem9  16370  gcdaddmlem  16493  sqnprm  16672  prmlem1  17078  prmlem2  17090  m1expaddsub  19473  psgnuni  19474  gzrngunitlem  21412  lmres  23265  zdis  24782  iihalf1  24898  lmclimf  25271  vitali  25580  ismbf  25595  ismbfcn  25596  mbfconst  25600  cncombf  25625  cnmbf  25626  limcfval  25839  dvnfre  25919  quotlem  26266  ulmval  26345  ulmpm  26348  abelthlem2  26397  abelthlem3  26398  abelthlem5  26400  abelthlem7  26403  efcvx  26414  logtayl  26624  logccv  26627  cxpcn3  26712  emcllem2  26960  zetacvg  26978  basellem5  27048  bposlem7  27253  chebbnd1lem3  27434  dchrisumlem3  27454  iscgrgd  28581  axcontlem2  29034  nv1  30746  blocnilem  30875  ipasslem8  30908  siii  30924  ubthlem1  30941  norm1  31320  hhshsslem2  31339  hoscli  31833  hodcli  31834  cnlnadjlem7  32144  adjbdln  32154  pjnmopi  32219  strlem1  32321  rexdiv  32985  tpr2rico  34056  qqhre  34164  signsply0  34695  subfacval3  35371  erdszelem4  35376  erdszelem8  35380  elmrsubrn  35702  rdgprc  35974  fwddifval  36344  fwddifnval  36345  exrecfnlem  37695  poimirlem29  37970  ismblfin  37982  itg2addnclem  37992  caures  38081  sswfaxreg  45414  nthrucw  47316  cjnpoly  47337  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem4  48595  iooii  49393  icccldii  49394