Theorem mpanl12 703

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  reuun1  4282  frminex  5611  tz6.26i  6314  wfii  6316  tfr2ALT  8342  tfr3ALT  8343  opthreg  9539  unsnen  10475  axcnre  11087  addgt0  11635  addgegt0  11636  addgtge0  11637  addge0  11638  addgt0i  11688  addge0i  11689  addgegt0i  11690  add20i  11692  mulge0i  11696  recextlem1  11779  recne0  11821  recdiv  11859  rec11i  11894  recgt1  12050  prodgt0i  12061  xadddi2  13224  iccshftri  13415  iccshftli  13417  iccdili  13419  icccntri  13421  mulexpz  14037  expaddz  14041  m1expeven  14044  iexpcyc  14142  cnpart  15175  resqrex  15185  sqreulem  15295  amgm2  15305  rlim  15430  ello12  15451  elo12  15462  bpolylem  15983  ege2le3  16025  dvdslelem  16248  divalglem1  16333  divalglem6  16337  divalglem9  16340  gcdaddmlem  16463  sqnprm  16641  prmlem1  17047  prmlem2  17059  m1expaddsub  19439  psgnuni  19440  gzrngunitlem  21399  lmres  23256  zdis  24773  iihalf1  24893  lmclimf  25272  vitali  25582  ismbf  25597  ismbfcn  25598  mbfconst  25602  cncombf  25627  cnmbf  25628  limcfval  25841  dvnfre  25924  quotlem  26276  ulmval  26357  ulmpm  26360  abelthlem2  26410  abelthlem3  26411  abelthlem5  26413  abelthlem7  26416  efcvx  26427  logtayl  26637  logccv  26640  cxpcn3  26726  emcllem2  26975  zetacvg  26993  basellem5  27063  bposlem7  27269  chebbnd1lem3  27450  dchrisumlem3  27470  iscgrgd  28597  axcontlem2  29050  nv1  30762  blocnilem  30891  ipasslem8  30924  siii  30940  ubthlem1  30957  norm1  31336  hhshsslem2  31355  hoscli  31849  hodcli  31850  cnlnadjlem7  32160  adjbdln  32170  pjnmopi  32235  strlem1  32337  rexdiv  33017  tpr2rico  34089  qqhre  34197  signsply0  34728  subfacval3  35402  erdszelem4  35407  erdszelem8  35411  elmrsubrn  35733  rdgprc  36005  fwddifval  36375  fwddifnval  36376  exrecfnlem  37628  poimirlem29  37894  ismblfin  37906  itg2addnclem  37916  caures  38005  sswfaxreg  45337  nthrucw  47238  cjnpoly  47243  pgnbgreunbgrlem1  48467  pgnbgreunbgrlem4  48473  iooii  49271  icccldii  49272