Theorem mpanl12 715

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  spcimgfi1  3511  reuun1  4273  frminex  5629  tz6.26i  6351  wfii  6353  tfr2ALT  8412  tfr3ALT  8413  opthreg  9622  unsnen  10640  axcnre  11252  addgt0  11805  addgegt0  11806  addgtge0  11807  addge0  11808  addgt0i  11858  addge0i  11859  addgegt0i  11860  add20i  11862  mulge0i  11866  recextlem1  11949  recne0  11990  recdiv  12026  rec11i  12061  recgt1  12216  prodgt0i  12227  xadddi2  13430  iccshftri  13621  iccshftli  13623  iccdili  13625  icccntri  13627  mulexpz  14248  expaddz  14252  m1expeven  14255  iexpcyc  14354  cnpart  15412  resqrex  15422  sqreulem  15532  amgm2  15542  rlim  15667  ello12  15688  elo12  15699  bpolylem  16219  ege2le3  16261  dvdslelem  16484  divalglem1  16569  divalglem6  16573  divalglem9  16576  gcdaddmlem  16701  sqnprm  16883  prmlem1  17290  prmlem2  17303  m1expaddsub  19717  psgnuni  19718  gzrngunitlem  21743  lmres  23623  zdis  25141  iihalf1  25257  lmclimf  25630  vitali  25939  ismbf  25954  ismbfcn  25955  mbfconst  25959  cncombf  25984  cnmbf  25985  limcfval  26197  dvnfre  26277  quotlem  26626  ulmval  26712  ulmpm  26715  abelthlem2  26764  abelthlem3  26765  abelthlem5  26767  abelthlem7  26770  efcvx  26781  logtayl  26993  logccv  26996  cxpcn3  27081  emcllem2  27329  zetacvg  27347  basellem5  27417  bposlem7  27622  chebbnd1lem3  27803  dchrisumlem3  27823  iscgrgd  28981  axcontlem2  29548  nv1  31282  blocnilem  31411  ipasslem8  31444  siii  31460  ubthlem1  31477  norm1  31856  hhshsslem2  31875  hoscli  32369  hodcli  32370  cnlnadjlem7  32680  adjbdln  32690  pjnmopi  32755  strlem1  32857  rexdiv  33538  tpr2rico  34590  qqhre  34698  signsply0  35226  subfacval3  36040  erdszelem4  36045  erdszelem8  36049  elmrsubrn  36371  rdgprc  36648  fwddifval  37019  fwddifnval  37020  exrecfnlem  38395  poimirlem29  38660  ismblfin  38672  itg2addnclem  38682  caures  38787  sswfaxreg  46070  cjnpoly  48032  pgnbgreunbgrlem1  49304  pgnbgreunbgrlem4  49310  iooii  50125  icccldii  50126