Theorem mpanl12 702

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 700	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 690	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:  reuun1  4278  frminex  5595  tz6.26i  6295  wfii  6297  tfr2ALT  8320  tfr3ALT  8321  opthreg  9508  unsnen  10441  axcnre  11052  addgt0  11600  addgegt0  11601  addgtge0  11602  addge0  11603  addgt0i  11653  addge0i  11654  addgegt0i  11655  add20i  11657  mulge0i  11661  recextlem1  11744  recne0  11786  recdiv  11824  rec11i  11859  recgt1  12015  prodgt0i  12026  xadddi2  13193  iccshftri  13384  iccshftli  13386  iccdili  13388  icccntri  13390  mulexpz  14006  expaddz  14010  m1expeven  14013  iexpcyc  14111  cnpart  15144  resqrex  15154  sqreulem  15264  amgm2  15274  rlim  15399  ello12  15420  elo12  15431  bpolylem  15952  ege2le3  15994  dvdslelem  16217  divalglem1  16302  divalglem6  16306  divalglem9  16309  gcdaddmlem  16432  sqnprm  16610  prmlem1  17016  prmlem2  17028  m1expaddsub  19408  psgnuni  19409  gzrngunitlem  21367  lmres  23213  zdis  24730  iihalf1  24850  lmclimf  25229  vitali  25539  ismbf  25554  ismbfcn  25555  mbfconst  25559  cncombf  25584  cnmbf  25585  limcfval  25798  dvnfre  25881  quotlem  26233  ulmval  26314  ulmpm  26317  abelthlem2  26367  abelthlem3  26368  abelthlem5  26370  abelthlem7  26373  efcvx  26384  logtayl  26594  logccv  26597  cxpcn3  26683  emcllem2  26932  zetacvg  26950  basellem5  27020  bposlem7  27226  chebbnd1lem3  27407  dchrisumlem3  27427  iscgrgd  28489  axcontlem2  28941  nv1  30650  blocnilem  30779  ipasslem8  30812  siii  30828  ubthlem1  30845  norm1  31224  hhshsslem2  31243  hoscli  31737  hodcli  31738  cnlnadjlem7  32048  adjbdln  32058  pjnmopi  32123  strlem1  32225  rexdiv  32901  tpr2rico  33920  qqhre  34028  signsply0  34559  subfacval3  35221  erdszelem4  35226  erdszelem8  35230  elmrsubrn  35552  rdgprc  35827  fwddifval  36195  fwddifnval  36196  exrecfnlem  37412  poimirlem29  37688  ismblfin  37700  itg2addnclem  37710  caures  37799  sswfaxreg  45019  cjnpoly  46919  pgnbgreunbgrlem1  48143  pgnbgreunbgrlem4  48149  iooii  48948  icccldii  48949