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  4281  frminex  5602  tz6.26i  6300  wfii  6302  tfr2ALT  8330  tfr3ALT  8331  opthreg  9533  unsnen  10466  axcnre  11077  addgt0  11624  addgegt0  11625  addgtge0  11626  addge0  11627  addgt0i  11677  addge0i  11678  addgegt0i  11679  add20i  11681  mulge0i  11685  recextlem1  11768  recne0  11810  recdiv  11848  rec11i  11883  recgt1  12039  prodgt0i  12050  xadddi2  13217  iccshftri  13408  iccshftli  13410  iccdili  13412  icccntri  13414  mulexpz  14027  expaddz  14031  m1expeven  14034  iexpcyc  14132  cnpart  15165  resqrex  15175  sqreulem  15285  amgm2  15295  rlim  15420  ello12  15441  elo12  15452  bpolylem  15973  ege2le3  16015  dvdslelem  16238  divalglem1  16323  divalglem6  16327  divalglem9  16330  gcdaddmlem  16453  sqnprm  16631  prmlem1  17037  prmlem2  17049  m1expaddsub  19395  psgnuni  19396  gzrngunitlem  21357  lmres  23203  zdis  24721  iihalf1  24841  lmclimf  25220  vitali  25530  ismbf  25545  ismbfcn  25546  mbfconst  25550  cncombf  25575  cnmbf  25576  limcfval  25789  dvnfre  25872  quotlem  26224  ulmval  26305  ulmpm  26308  abelthlem2  26358  abelthlem3  26359  abelthlem5  26361  abelthlem7  26364  efcvx  26375  logtayl  26585  logccv  26588  cxpcn3  26674  emcllem2  26923  zetacvg  26941  basellem5  27011  bposlem7  27217  chebbnd1lem3  27398  dchrisumlem3  27418  iscgrgd  28476  axcontlem2  28928  nv1  30637  blocnilem  30766  ipasslem8  30799  siii  30815  ubthlem1  30832  norm1  31211  hhshsslem2  31230  hoscli  31724  hodcli  31725  cnlnadjlem7  32035  adjbdln  32045  pjnmopi  32110  strlem1  32212  rexdiv  32879  tpr2rico  33878  qqhre  33986  signsply0  34518  subfacval3  35161  erdszelem4  35166  erdszelem8  35170  elmrsubrn  35492  rdgprc  35767  fwddifval  36135  fwddifnval  36136  exrecfnlem  37352  poimirlem29  37628  ismblfin  37640  itg2addnclem  37650  caures  37739  sswfaxreg  44961  cjnpoly  46874  pgnbgreunbgrlem1  48098  pgnbgreunbgrlem4  48104  iooii  48903  icccldii  48904