Theorem mpanl12 700

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  reuun1  4282  frminex  5618  tz6.26i  6308  wfii  6311  wfr3OLD  8289  tfr2ALT  8352  tfr3ALT  8353  opthreg  9563  unsnen  10498  axcnre  11109  addgt0  11650  addgegt0  11651  addgtge0  11652  addge0  11653  addgt0i  11703  addge0i  11704  addgegt0i  11705  add20i  11707  mulge0i  11711  recextlem1  11794  recne0  11835  recdiv  11870  rec11i  11905  recgt1  12060  prodgt0i  12071  xadddi2  13226  iccshftri  13414  iccshftli  13416  iccdili  13418  icccntri  13420  mulexpz  14018  expaddz  14022  m1expeven  14025  iexpcyc  14121  cnpart  15137  resqrex  15147  sqreulem  15256  amgm2  15266  rlim  15389  ello12  15410  elo12  15421  bpolylem  15942  ege2le3  15983  dvdslelem  16202  divalglem1  16287  divalglem6  16291  divalglem9  16294  gcdaddmlem  16415  sqnprm  16589  prmlem1  16991  prmlem2  17003  m1expaddsub  19294  psgnuni  19295  gzrngunitlem  20899  lmres  22688  zdis  24216  iihalf1  24331  lmclimf  24705  vitali  25014  ismbf  25029  ismbfcn  25030  mbfconst  25034  cncombf  25059  cnmbf  25060  limcfval  25273  dvnfre  25353  quotlem  25697  ulmval  25776  ulmpm  25779  abelthlem2  25828  abelthlem3  25829  abelthlem5  25831  abelthlem7  25834  efcvx  25845  logtayl  26052  logccv  26055  cxpcn3  26138  emcllem2  26383  zetacvg  26401  basellem5  26471  bposlem7  26675  chebbnd1lem3  26856  dchrisumlem3  26876  iscgrgd  27518  axcontlem2  27977  nv1  29680  blocnilem  29809  ipasslem8  29842  siii  29858  ubthlem1  29875  norm1  30254  hhshsslem2  30273  hoscli  30767  hodcli  30768  cnlnadjlem7  31078  adjbdln  31088  pjnmopi  31153  strlem1  31255  rexdiv  31852  tpr2rico  32582  qqhre  32690  signsply0  33252  subfacval3  33870  erdszelem4  33875  erdszelem8  33879  elmrsubrn  34201  rdgprc  34455  fwddifval  34823  fwddifnval  34824  exrecfnlem  35923  poimirlem29  36180  ismblfin  36192  itg2addnclem  36202  caures  36292  iooii  47070  icccldii  47071