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  3515  reuun1  4276  frminex  5635  tz6.26i  6372  wfii  6374  tfr2ALT  8440  tfr3ALT  8441  opthreg  9649  unsnen  10667  axcnre  11279  addgt0  11832  addgegt0  11833  addgtge0  11834  addge0  11835  addgt0i  11885  addge0i  11886  addgegt0i  11887  add20i  11889  mulge0i  11893  recextlem1  11976  recne0  12017  recdiv  12053  rec11i  12088  recgt1  12243  prodgt0i  12254  xadddi2  13457  iccshftri  13648  iccshftli  13650  iccdili  13652  icccntri  13654  mulexpz  14275  expaddz  14279  m1expeven  14282  iexpcyc  14381  cnpart  15439  resqrex  15449  sqreulem  15559  amgm2  15569  rlim  15694  ello12  15715  elo12  15726  bpolylem  16246  ege2le3  16288  dvdslelem  16511  divalglem1  16596  divalglem6  16600  divalglem9  16603  gcdaddmlem  16728  sqnprm  16910  prmlem1  17317  prmlem2  17330  m1expaddsub  19745  psgnuni  19746  gzrngunitlem  21771  lmres  23651  zdis  25169  iihalf1  25285  lmclimf  25658  vitali  25967  ismbf  25982  ismbfcn  25983  mbfconst  25987  cncombf  26012  cnmbf  26013  limcfval  26225  dvnfre  26305  quotlem  26654  ulmval  26740  ulmpm  26743  abelthlem2  26792  abelthlem3  26793  abelthlem5  26795  abelthlem7  26798  efcvx  26809  logtayl  27021  logccv  27024  cxpcn3  27109  emcllem2  27357  zetacvg  27375  basellem5  27445  bposlem7  27650  chebbnd1lem3  27831  dchrisumlem3  27851  iscgrgd  29009  axcontlem2  29576  nv1  31310  blocnilem  31439  ipasslem8  31472  siii  31488  ubthlem1  31505  norm1  31884  hhshsslem2  31903  hoscli  32397  hodcli  32398  cnlnadjlem7  32708  adjbdln  32718  pjnmopi  32783  strlem1  32885  rexdiv  33565  tpr2rico  34627  qqhre  34735  signsply0  35263  subfacval3  36134  erdszelem4  36139  erdszelem8  36143  elmrsubrn  36465  rdgprc  36747  fwddifval  37118  fwddifnval  37119  exrecfnlem  38507  poimirlem29  38772  ismblfin  38784  itg2addnclem  38794  caures  38897  sswfaxreg  46183  cjnpoly  48154  pgnbgreunbgrlem1  49426  pgnbgreunbgrlem4  49432  iooii  50247  icccldii  50248