Theorem mpanl12 700

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  reuun1  4285  frminex  5530  tz6.26i  6175  wfii  6177  opthreg  9075  unsnen  9969  axcnre  10580  addgt0  11120  addgegt0  11121  addgtge0  11122  addge0  11123  addgt0i  11173  addge0i  11174  addgegt0i  11175  add20i  11177  mulge0i  11181  recextlem1  11264  recne0  11305  recdiv  11340  rec11i  11375  recgt1  11530  prodgt0i  11541  xadddi2  12684  iccshftri  12867  iccshftli  12869  iccdili  12871  icccntri  12873  mulexpz  13463  expaddz  13467  m1expeven  13470  iexpcyc  13563  cnpart  14593  resqrex  14604  sqreulem  14713  amgm2  14723  rlim  14846  ello12  14867  elo12  14878  ege2le3  15437  dvdslelem  15653  divalglem1  15739  divalglem6  15743  divalglem9  15746  gcdaddmlem  15866  sqnprm  16040  prmlem1  16435  prmlem2  16447  m1expaddsub  18620  psgnuni  18621  gzrngunitlem  20604  lmres  21902  zdis  23418  iihalf1  23529  lmclimf  23901  vitali  24208  ismbf  24223  ismbfcn  24224  mbfconst  24228  cncombf  24253  cnmbf  24254  limcfval  24464  dvnfre  24543  quotlem  24883  ulmval  24962  ulmpm  24965  abelthlem2  25014  abelthlem3  25015  abelthlem5  25017  abelthlem7  25020  efcvx  25031  logtayl  25237  logccv  25240  cxpcn3  25323  emcllem2  25568  zetacvg  25586  basellem5  25656  bposlem7  25860  chebbnd1lem3  26041  dchrisumlem3  26061  iscgrgd  26293  axcontlem2  26745  nv1  28446  blocnilem  28575  ipasslem8  28608  siii  28624  ubthlem1  28641  norm1  29020  hhshsslem2  29039  hoscli  29533  hodcli  29534  cnlnadjlem7  29844  adjbdln  29854  pjnmopi  29919  strlem1  30021  rexdiv  30597  tpr2rico  31150  qqhre  31256  signsply0  31816  subfacval3  32431  erdszelem4  32436  erdszelem8  32440  elmrsubrn  32762  rdgprc  33034  frindi  33081  fwddifval  33618  fwddifnval  33619  exrecfnlem  34654  poimirlem29  34915  ismblfin  34927  itg2addnclem  34937  caures  35029