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  3519  reuun1  4284  frminex  5645  tz6.26i  6356  wfii  6358  tfr2ALT  8397  tfr3ALT  8398  opthreg  9597  unsnen  10555  axcnre  11167  addgt0  11718  addgegt0  11719  addgtge0  11720  addge0  11721  addgt0i  11771  addge0i  11772  addgegt0i  11773  add20i  11775  mulge0i  11779  recextlem1  11862  recne0  11903  recdiv  11939  rec11i  11974  recgt1  12129  prodgt0i  12140  xadddi2  13341  iccshftri  13532  iccshftli  13534  iccdili  13536  icccntri  13538  mulexpz  14158  expaddz  14162  m1expeven  14165  iexpcyc  14263  cnpart  15317  resqrex  15327  sqreulem  15437  amgm2  15447  rlim  15572  ello12  15593  elo12  15604  bpolylem  16127  ege2le3  16169  dvdslelem  16392  divalglem1  16477  divalglem6  16481  divalglem9  16484  gcdaddmlem  16607  sqnprm  16786  prmlem1  17192  prmlem2  17205  m1expaddsub  19599  psgnuni  19600  gzrngunitlem  21619  lmres  23494  zdis  25011  iihalf1  25127  lmclimf  25500  vitali  25809  ismbf  25824  ismbfcn  25825  mbfconst  25829  cncombf  25854  cnmbf  25855  limcfval  26068  dvnfre  26148  quotlem  26498  ulmval  26580  ulmpm  26583  abelthlem2  26632  abelthlem3  26633  abelthlem5  26635  abelthlem7  26638  efcvx  26649  logtayl  26862  logccv  26865  cxpcn3  26950  emcllem2  27198  zetacvg  27216  basellem5  27286  bposlem7  27491  chebbnd1lem3  27672  dchrisumlem3  27692  iscgrgd  28819  axcontlem2  29352  nv1  31064  blocnilem  31193  ipasslem8  31226  siii  31242  ubthlem1  31259  norm1  31638  hhshsslem2  31657  hoscli  32151  hodcli  32152  cnlnadjlem7  32462  adjbdln  32472  pjnmopi  32537  strlem1  32639  rexdiv  33282  tpr2rico  34333  qqhre  34441  signsply0  34970  subfacval3  35702  erdszelem4  35707  erdszelem8  35711  elmrsubrn  36033  rdgprc  36305  fwddifval  36675  fwddifnval  36676  exrecfnlem  38066  poimirlem29  38341  ismblfin  38353  itg2addnclem  38363  caures  38452  sswfaxreg  45737  cjnpoly  47667  pgnbgreunbgrlem1  48919  pgnbgreunbgrlem4  48925  iooii  49737  icccldii  49738