Theorem mpanl12 702

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 700	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 690	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  4294  frminex  5620  tz6.26i  6324  wfii  6326  tfr2ALT  8372  tfr3ALT  8373  opthreg  9578  unsnen  10513  axcnre  11124  addgt0  11671  addgegt0  11672  addgtge0  11673  addge0  11674  addgt0i  11724  addge0i  11725  addgegt0i  11726  add20i  11728  mulge0i  11732  recextlem1  11815  recne0  11857  recdiv  11895  rec11i  11930  recgt1  12086  prodgt0i  12097  xadddi2  13264  iccshftri  13455  iccshftli  13457  iccdili  13459  icccntri  13461  mulexpz  14074  expaddz  14078  m1expeven  14081  iexpcyc  14179  cnpart  15213  resqrex  15223  sqreulem  15333  amgm2  15343  rlim  15468  ello12  15489  elo12  15500  bpolylem  16021  ege2le3  16063  dvdslelem  16286  divalglem1  16371  divalglem6  16375  divalglem9  16378  gcdaddmlem  16501  sqnprm  16679  prmlem1  17085  prmlem2  17097  m1expaddsub  19435  psgnuni  19436  gzrngunitlem  21356  lmres  23194  zdis  24712  iihalf1  24832  lmclimf  25211  vitali  25521  ismbf  25536  ismbfcn  25537  mbfconst  25541  cncombf  25566  cnmbf  25567  limcfval  25780  dvnfre  25863  quotlem  26215  ulmval  26296  ulmpm  26299  abelthlem2  26349  abelthlem3  26350  abelthlem5  26352  abelthlem7  26355  efcvx  26366  logtayl  26576  logccv  26579  cxpcn3  26665  emcllem2  26914  zetacvg  26932  basellem5  27002  bposlem7  27208  chebbnd1lem3  27389  dchrisumlem3  27409  iscgrgd  28447  axcontlem2  28899  nv1  30611  blocnilem  30740  ipasslem8  30773  siii  30789  ubthlem1  30806  norm1  31185  hhshsslem2  31204  hoscli  31698  hodcli  31699  cnlnadjlem7  32009  adjbdln  32019  pjnmopi  32084  strlem1  32186  rexdiv  32853  tpr2rico  33909  qqhre  34017  signsply0  34549  subfacval3  35183  erdszelem4  35188  erdszelem8  35192  elmrsubrn  35514  rdgprc  35789  fwddifval  36157  fwddifnval  36158  exrecfnlem  37374  poimirlem29  37650  ismblfin  37662  itg2addnclem  37672  caures  37761  sswfaxreg  44984  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem4  48113  iooii  48910  icccldii  48911