Theorem mpanl12 720

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  reuun1  4052  frminex  5246  tz6.26i  5873  wfii  5875  opthreg  8686  opthregOLD  8688  unsnen  9567  axcnre  10177  addgt0  10706  addgegt0  10707  addgtge0  10708  addge0  10709  addgt0i  10759  addge0i  10760  addgegt0i  10761  add20i  10763  mulge0i  10767  recextlem1  10849  recne0  10890  recdiv  10923  rec11i  10958  recgt1  11111  prodgt0i  11122  prodge0i  11123  xadddi2  12320  iccshftri  12500  iccshftli  12502  iccdili  12504  icccntri  12506  mulexpz  13094  expaddz  13098  m1expeven  13101  iexpcyc  13163  cnpart  14179  resqrex  14190  sqreulem  14298  amgm2  14308  rlim  14425  ello12  14446  elo12  14457  efcllem  15007  ege2le3  15019  dvdslelem  15233  divalglem1  15319  divalglem6  15323  divalglem9  15326  gcdaddmlem  15447  sqnprm  15616  prmlem1  16016  prmlem2  16029  xpscfn  16421  m1expaddsub  18118  psgnuni  18119  gzrngunitlem  20013  lmres  21306  zdis  22820  iihalf1  22931  lmclimf  23302  vitali  23581  ismbf  23596  ismbfcn  23597  mbfconst  23601  cncombf  23624  cnmbf  23625  limcfval  23835  dvnfre  23914  quotlem  24254  ulmval  24333  ulmpm  24336  abelthlem2  24385  abelthlem3  24386  abelthlem5  24388  abelthlem7  24391  efcvx  24402  logtayl  24605  logccv  24608  cxpcn3  24688  emcllem2  24922  zetacvg  24940  basellem5  25010  bposlem7  25214  chebbnd1lem3  25359  dchrisumlem3  25379  iscgrgd  25607  axcontlem2  26044  nv1  27839  blocnilem  27968  ipasslem8  28001  siii  28017  ubthlem1  28035  norm1  28415  hhshsslem2  28434  hoscli  28930  hodcli  28931  cnlnadjlem7  29241  adjbdln  29251  pjnmopi  29316  strlem1  29418  rexdiv  29943  tpr2rico  30267  qqhre  30373  signsply0  30937  subfacval3  31478  erdszelem4  31483  erdszelem8  31487  elmrsubrn  31724  rdgprc  32005  frindi  32050  fwddifval  32575  fwddifnval  32576  poimirlem29  33751  ismblfin  33763  itg2addnclem  33774  caures  33869