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  8409  tfr3ALT  8410  opthreg  9619  unsnen  10637  axcnre  11249  addgt0  11802  addgegt0  11803  addgtge0  11804  addge0  11805  addgt0i  11855  addge0i  11856  addgegt0i  11857  add20i  11859  mulge0i  11863  recextlem1  11946  recne0  11987  recdiv  12023  rec11i  12058  recgt1  12213  prodgt0i  12224  xadddi2  13427  iccshftri  13618  iccshftli  13620  iccdili  13622  icccntri  13624  mulexpz  14245  expaddz  14249  m1expeven  14252  iexpcyc  14351  cnpart  15407  resqrex  15417  sqreulem  15527  amgm2  15537  rlim  15662  ello12  15683  elo12  15694  bpolylem  16214  ege2le3  16256  dvdslelem  16479  divalglem1  16564  divalglem6  16568  divalglem9  16571  gcdaddmlem  16696  sqnprm  16878  prmlem1  17285  prmlem2  17298  m1expaddsub  19712  psgnuni  19713  gzrngunitlem  21738  lmres  23618  zdis  25136  iihalf1  25252  lmclimf  25625  vitali  25934  ismbf  25949  ismbfcn  25950  mbfconst  25954  cncombf  25979  cnmbf  25980  limcfval  26192  dvnfre  26272  quotlem  26621  ulmval  26707  ulmpm  26710  abelthlem2  26759  abelthlem3  26760  abelthlem5  26762  abelthlem7  26765  efcvx  26776  logtayl  26988  logccv  26991  cxpcn3  27076  emcllem2  27324  zetacvg  27342  basellem5  27412  bposlem7  27617  chebbnd1lem3  27798  dchrisumlem3  27818  iscgrgd  28976  axcontlem2  29543  nv1  31277  blocnilem  31406  ipasslem8  31439  siii  31455  ubthlem1  31472  norm1  31851  hhshsslem2  31870  hoscli  32364  hodcli  32365  cnlnadjlem7  32675  adjbdln  32685  pjnmopi  32750  strlem1  32852  rexdiv  33534  tpr2rico  34586  qqhre  34694  signsply0  35222  subfacval3  35996  erdszelem4  36001  erdszelem8  36005  elmrsubrn  36327  rdgprc  36598  fwddifval  36969  fwddifnval  36970  exrecfnlem  38345  poimirlem29  38610  ismblfin  38622  itg2addnclem  38632  caures  38737  sswfaxreg  46019  cjnpoly  47981  pgnbgreunbgrlem1  49253  pgnbgreunbgrlem4  49259  iooii  50068  icccldii  50069