Theorem mpanl12 712

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  spcimgfi1  3514  reuun1  4280  frminex  5624  tz6.26i  6331  wfii  6333  tfr2ALT  8367  tfr3ALT  8368  opthreg  9570  unsnen  10507  axcnre  11119  addgt0  11670  addgegt0  11671  addgtge0  11672  addge0  11673  addgt0i  11723  addge0i  11724  addgegt0i  11725  add20i  11727  mulge0i  11731  recextlem1  11814  recne0  11855  recdiv  11894  rec11i  11929  recgt1  12085  prodgt0i  12096  xadddi2  13297  iccshftri  13488  iccshftli  13490  iccdili  13492  icccntri  13494  mulexpz  14112  expaddz  14116  m1expeven  14119  iexpcyc  14217  cnpart  15250  resqrex  15260  sqreulem  15370  amgm2  15380  rlim  15505  ello12  15526  elo12  15537  bpolylem  16061  ege2le3  16103  dvdslelem  16326  divalglem1  16411  divalglem6  16415  divalglem9  16418  gcdaddmlem  16541  sqnprm  16720  prmlem1  17126  prmlem2  17139  m1expaddsub  19521  psgnuni  19522  gzrngunitlem  21464  lmres  23340  zdis  24857  iihalf1  24973  lmclimf  25346  vitali  25655  ismbf  25670  ismbfcn  25671  mbfconst  25675  cncombf  25700  cnmbf  25701  limcfval  25914  dvnfre  25994  quotlem  26341  ulmval  26420  ulmpm  26423  abelthlem2  26472  abelthlem3  26473  abelthlem5  26475  abelthlem7  26478  efcvx  26489  logtayl  26702  logccv  26705  cxpcn3  26790  emcllem2  27038  zetacvg  27056  basellem5  27126  bposlem7  27331  chebbnd1lem3  27512  dchrisumlem3  27532  iscgrgd  28659  axcontlem2  29112  nv1  30824  blocnilem  30953  ipasslem8  30986  siii  31002  ubthlem1  31019  norm1  31398  hhshsslem2  31417  hoscli  31911  hodcli  31912  cnlnadjlem7  32222  adjbdln  32232  pjnmopi  32297  strlem1  32399  rexdiv  33064  tpr2rico  34170  qqhre  34278  signsply0  34809  subfacval3  35503  erdszelem4  35508  erdszelem8  35512  elmrsubrn  35834  rdgprc  36106  fwddifval  36476  fwddifnval  36477  exrecfnlem  37837  poimirlem29  38112  ismblfin  38124  itg2addnclem  38134  caures  38223  sswfaxreg  45527  nthrucw  47426  cjnpoly  47447  pgnbgreunbgrlem1  48699  pgnbgreunbgrlem4  48705  iooii  49503  icccldii  49504