Theorem mpanl12 701

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 699	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 689	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  4347  frminex  5679  tz6.26i  6381  wfii  6384  wfr3OLD  8394  tfr2ALT  8457  tfr3ALT  8458  opthreg  9687  unsnen  10622  axcnre  11233  addgt0  11776  addgegt0  11777  addgtge0  11778  addge0  11779  addgt0i  11829  addge0i  11830  addgegt0i  11831  add20i  11833  mulge0i  11837  recextlem1  11920  recne0  11962  recdiv  12000  rec11i  12035  recgt1  12191  prodgt0i  12202  xadddi2  13359  iccshftri  13547  iccshftli  13549  iccdili  13551  icccntri  13553  mulexpz  14153  expaddz  14157  m1expeven  14160  iexpcyc  14256  cnpart  15289  resqrex  15299  sqreulem  15408  amgm2  15418  rlim  15541  ello12  15562  elo12  15573  bpolylem  16096  ege2le3  16138  dvdslelem  16357  divalglem1  16442  divalglem6  16446  divalglem9  16449  gcdaddmlem  16570  sqnprm  16749  prmlem1  17155  prmlem2  17167  m1expaddsub  19540  psgnuni  19541  gzrngunitlem  21473  lmres  23329  zdis  24857  iihalf1  24977  lmclimf  25357  vitali  25667  ismbf  25682  ismbfcn  25683  mbfconst  25687  cncombf  25712  cnmbf  25713  limcfval  25927  dvnfre  26010  quotlem  26360  ulmval  26441  ulmpm  26444  abelthlem2  26494  abelthlem3  26495  abelthlem5  26497  abelthlem7  26500  efcvx  26511  logtayl  26720  logccv  26723  cxpcn3  26809  emcllem2  27058  zetacvg  27076  basellem5  27146  bposlem7  27352  chebbnd1lem3  27533  dchrisumlem3  27553  iscgrgd  28539  axcontlem2  28998  nv1  30707  blocnilem  30836  ipasslem8  30869  siii  30885  ubthlem1  30902  norm1  31281  hhshsslem2  31300  hoscli  31794  hodcli  31795  cnlnadjlem7  32105  adjbdln  32115  pjnmopi  32180  strlem1  32282  rexdiv  32890  tpr2rico  33858  qqhre  33966  signsply0  34528  subfacval3  35157  erdszelem4  35162  erdszelem8  35166  elmrsubrn  35488  rdgprc  35758  fwddifval  36126  fwddifnval  36127  exrecfnlem  37345  poimirlem29  37609  ismblfin  37621  itg2addnclem  37631  caures  37720  iooii  48597  icccldii  48598