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  3493  reuun1  4269  frminex  5603  tz6.26i  6306  wfii  6308  tfr2ALT  8333  tfr3ALT  8334  opthreg  9530  unsnen  10466  axcnre  11078  addgt0  11627  addgegt0  11628  addgtge0  11629  addge0  11630  addgt0i  11680  addge0i  11681  addgegt0i  11682  add20i  11684  mulge0i  11688  recextlem1  11771  recne0  11813  recdiv  11852  rec11i  11887  recgt1  12043  prodgt0i  12054  xadddi2  13240  iccshftri  13431  iccshftli  13433  iccdili  13435  icccntri  13437  mulexpz  14055  expaddz  14059  m1expeven  14062  iexpcyc  14160  cnpart  15193  resqrex  15203  sqreulem  15313  amgm2  15323  rlim  15448  ello12  15469  elo12  15480  bpolylem  16004  ege2le3  16046  dvdslelem  16269  divalglem1  16354  divalglem6  16358  divalglem9  16361  gcdaddmlem  16484  sqnprm  16663  prmlem1  17069  prmlem2  17081  m1expaddsub  19464  psgnuni  19465  gzrngunitlem  21422  lmres  23275  zdis  24792  iihalf1  24908  lmclimf  25281  vitali  25590  ismbf  25605  ismbfcn  25606  mbfconst  25610  cncombf  25635  cnmbf  25636  limcfval  25849  dvnfre  25929  quotlem  26277  ulmval  26358  ulmpm  26361  abelthlem2  26410  abelthlem3  26411  abelthlem5  26413  abelthlem7  26416  efcvx  26427  logtayl  26637  logccv  26640  cxpcn3  26725  emcllem2  26974  zetacvg  26992  basellem5  27062  bposlem7  27267  chebbnd1lem3  27448  dchrisumlem3  27468  iscgrgd  28595  axcontlem2  29048  nv1  30761  blocnilem  30890  ipasslem8  30923  siii  30939  ubthlem1  30956  norm1  31335  hhshsslem2  31354  hoscli  31848  hodcli  31849  cnlnadjlem7  32159  adjbdln  32169  pjnmopi  32234  strlem1  32336  rexdiv  33000  tpr2rico  34072  qqhre  34180  signsply0  34711  subfacval3  35387  erdszelem4  35392  erdszelem8  35396  elmrsubrn  35718  rdgprc  35990  fwddifval  36360  fwddifnval  36361  exrecfnlem  37709  poimirlem29  37984  ismblfin  37996  itg2addnclem  38006  caures  38095  sswfaxreg  45432  nthrucw  47332  cjnpoly  47349  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem4  48607  iooii  49405  icccldii  49406