Theorem mpanl12 698

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 696	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 686	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 206  df-an 396

This theorem is referenced by:  reuun1  4248  frminex  5560  tz6.26i  6237  wfii  6240  wfr3OLD  8140  tfr2ALT  8203  tfr3ALT  8204  opthreg  9306  unsnen  10240  axcnre  10851  addgt0  11391  addgegt0  11392  addgtge0  11393  addge0  11394  addgt0i  11444  addge0i  11445  addgegt0i  11446  add20i  11448  mulge0i  11452  recextlem1  11535  recne0  11576  recdiv  11611  rec11i  11646  recgt1  11801  prodgt0i  11812  xadddi2  12960  iccshftri  13148  iccshftli  13150  iccdili  13152  icccntri  13154  mulexpz  13751  expaddz  13755  m1expeven  13758  iexpcyc  13851  cnpart  14879  resqrex  14890  sqreulem  14999  amgm2  15009  rlim  15132  ello12  15153  elo12  15164  bpolylem  15686  ege2le3  15727  dvdslelem  15946  divalglem1  16031  divalglem6  16035  divalglem9  16038  gcdaddmlem  16159  sqnprm  16335  prmlem1  16737  prmlem2  16749  m1expaddsub  19021  psgnuni  19022  gzrngunitlem  20575  lmres  22359  zdis  23885  iihalf1  24000  lmclimf  24373  vitali  24682  ismbf  24697  ismbfcn  24698  mbfconst  24702  cncombf  24727  cnmbf  24728  limcfval  24941  dvnfre  25021  quotlem  25365  ulmval  25444  ulmpm  25447  abelthlem2  25496  abelthlem3  25497  abelthlem5  25499  abelthlem7  25502  efcvx  25513  logtayl  25720  logccv  25723  cxpcn3  25806  emcllem2  26051  zetacvg  26069  basellem5  26139  bposlem7  26343  chebbnd1lem3  26524  dchrisumlem3  26544  iscgrgd  26778  axcontlem2  27236  nv1  28938  blocnilem  29067  ipasslem8  29100  siii  29116  ubthlem1  29133  norm1  29512  hhshsslem2  29531  hoscli  30025  hodcli  30026  cnlnadjlem7  30336  adjbdln  30346  pjnmopi  30411  strlem1  30513  rexdiv  31102  tpr2rico  31764  qqhre  31870  signsply0  32430  subfacval3  33051  erdszelem4  33056  erdszelem8  33060  elmrsubrn  33382  rdgprc  33676  fwddifval  34391  fwddifnval  34392  exrecfnlem  35477  poimirlem29  35733  ismblfin  35745  itg2addnclem  35755  caures  35845  iooii  46099  icccldii  46100