Theorem mpanl12 699

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  reuun1  4252  frminex  5570  tz6.26i  6256  wfii  6259  wfr3OLD  8178  tfr2ALT  8241  tfr3ALT  8242  opthreg  9385  unsnen  10318  axcnre  10929  addgt0  11470  addgegt0  11471  addgtge0  11472  addge0  11473  addgt0i  11523  addge0i  11524  addgegt0i  11525  add20i  11527  mulge0i  11531  recextlem1  11614  recne0  11655  recdiv  11690  rec11i  11725  recgt1  11880  prodgt0i  11891  xadddi2  13040  iccshftri  13228  iccshftli  13230  iccdili  13232  icccntri  13234  mulexpz  13832  expaddz  13836  m1expeven  13839  iexpcyc  13932  cnpart  14960  resqrex  14971  sqreulem  15080  amgm2  15090  rlim  15213  ello12  15234  elo12  15245  bpolylem  15767  ege2le3  15808  dvdslelem  16027  divalglem1  16112  divalglem6  16116  divalglem9  16119  gcdaddmlem  16240  sqnprm  16416  prmlem1  16818  prmlem2  16830  m1expaddsub  19115  psgnuni  19116  gzrngunitlem  20672  lmres  22460  zdis  23988  iihalf1  24103  lmclimf  24477  vitali  24786  ismbf  24801  ismbfcn  24802  mbfconst  24806  cncombf  24831  cnmbf  24832  limcfval  25045  dvnfre  25125  quotlem  25469  ulmval  25548  ulmpm  25551  abelthlem2  25600  abelthlem3  25601  abelthlem5  25603  abelthlem7  25606  efcvx  25617  logtayl  25824  logccv  25827  cxpcn3  25910  emcllem2  26155  zetacvg  26173  basellem5  26243  bposlem7  26447  chebbnd1lem3  26628  dchrisumlem3  26648  iscgrgd  26883  axcontlem2  27342  nv1  29046  blocnilem  29175  ipasslem8  29208  siii  29224  ubthlem1  29241  norm1  29620  hhshsslem2  29639  hoscli  30133  hodcli  30134  cnlnadjlem7  30444  adjbdln  30454  pjnmopi  30519  strlem1  30621  rexdiv  31209  tpr2rico  31871  qqhre  31979  signsply0  32539  subfacval3  33160  erdszelem4  33165  erdszelem8  33169  elmrsubrn  33491  rdgprc  33779  fwddifval  34473  fwddifnval  34474  exrecfnlem  35559  poimirlem29  35815  ismblfin  35827  itg2addnclem  35837  caures  35927  iooii  46222  icccldii  46223