Theorem mpanl12 692

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  reuun1  4134  frminex  5335  tz6.26i  5965  wfii  5967  opthreg  8810  opthregOLD  8812  unsnen  9710  axcnre  10321  addgt0  10861  addgegt0  10862  addgtge0  10863  addge0  10864  addgt0i  10914  addge0i  10915  addgegt0i  10916  add20i  10918  mulge0i  10922  recextlem1  11005  recne0  11046  recdiv  11081  rec11i  11116  recgt1  11273  prodgt0i  11284  prodge0iOLD  11285  xadddi2  12439  iccshftri  12624  iccshftli  12626  iccdili  12628  icccntri  12630  mulexpz  13218  expaddz  13222  m1expeven  13225  iexpcyc  13288  cnpart  14387  resqrex  14398  sqreulem  14506  amgm2  14516  rlim  14634  ello12  14655  elo12  14666  ege2le3  15222  dvdslelem  15438  divalglem1  15524  divalglem6  15528  divalglem9  15531  gcdaddmlem  15651  sqnprm  15818  prmlem1  16213  prmlem2  16225  xpscfn  16605  m1expaddsub  18302  psgnuni  18303  gzrngunitlem  20207  lmres  21512  zdis  23027  iihalf1  23138  lmclimf  23510  vitali  23817  ismbf  23832  ismbfcn  23833  mbfconst  23837  cncombf  23862  cnmbf  23863  limcfval  24073  dvnfre  24152  quotlem  24492  ulmval  24571  ulmpm  24574  abelthlem2  24623  abelthlem3  24624  abelthlem5  24626  abelthlem7  24629  efcvx  24640  logtayl  24843  logccv  24846  cxpcn3  24929  emcllem2  25175  zetacvg  25193  basellem5  25263  bposlem7  25467  chebbnd1lem3  25612  dchrisumlem3  25632  iscgrgd  25864  axcontlem2  26314  nv1  28102  blocnilem  28231  ipasslem8  28264  siii  28280  ubthlem1  28298  norm1  28678  hhshsslem2  28697  hoscli  29193  hodcli  29194  cnlnadjlem7  29504  adjbdln  29514  pjnmopi  29579  strlem1  29681  rexdiv  30196  tpr2rico  30556  qqhre  30662  signsply0  31228  subfacval3  31770  erdszelem4  31775  erdszelem8  31779  elmrsubrn  32016  rdgprc  32288  frindi  32333  fwddifval  32858  fwddifnval  32859  poimirlem29  34048  ismblfin  34060  itg2addnclem  34070  caures  34164