Theorem mpanl12 708

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

This theorem is referenced by:  spcimgfi1  3495  reuun1  4263  frminex  5604  tz6.26i  6306  wfii  6308  tfr2ALT  8337  tfr3ALT  8338  opthreg  9537  unsnen  10473  axcnre  11085  addgt0  11634  addgegt0  11635  addgtge0  11636  addge0  11637  addgt0i  11687  addge0i  11688  addgegt0i  11689  add20i  11691  mulge0i  11695  recextlem1  11778  recne0  11820  recdiv  11859  rec11i  11894  recgt1  12050  prodgt0i  12061  xadddi2  13247  iccshftri  13438  iccshftli  13440  iccdili  13442  icccntri  13444  mulexpz  14062  expaddz  14066  m1expeven  14069  iexpcyc  14167  cnpart  15200  resqrex  15210  sqreulem  15320  amgm2  15330  rlim  15455  ello12  15476  elo12  15487  bpolylem  16011  ege2le3  16053  dvdslelem  16276  divalglem1  16361  divalglem6  16365  divalglem9  16368  gcdaddmlem  16491  sqnprm  16670  prmlem1  17076  prmlem2  17088  m1expaddsub  19471  psgnuni  19472  gzrngunitlem  21414  lmres  23290  zdis  24807  iihalf1  24923  lmclimf  25296  vitali  25605  ismbf  25620  ismbfcn  25621  mbfconst  25625  cncombf  25650  cnmbf  25651  limcfval  25864  dvnfre  25944  quotlem  26291  ulmval  26370  ulmpm  26373  abelthlem2  26422  abelthlem3  26423  abelthlem5  26425  abelthlem7  26428  efcvx  26439  logtayl  26649  logccv  26652  cxpcn3  26737  emcllem2  26985  zetacvg  27003  basellem5  27073  bposlem7  27278  chebbnd1lem3  27459  dchrisumlem3  27479  iscgrgd  28606  axcontlem2  29059  nv1  30771  blocnilem  30900  ipasslem8  30933  siii  30949  ubthlem1  30966  norm1  31345  hhshsslem2  31364  hoscli  31858  hodcli  31859  cnlnadjlem7  32169  adjbdln  32179  pjnmopi  32244  strlem1  32346  rexdiv  33011  tpr2rico  34103  qqhre  34211  signsply0  34742  subfacval3  35424  erdszelem4  35429  erdszelem8  35433  elmrsubrn  35755  rdgprc  36027  fwddifval  36397  fwddifnval  36398  exrecfnlem  37748  poimirlem29  38023  ismblfin  38035  itg2addnclem  38045  caures  38134  sswfaxreg  45438  nthrucw  47338  cjnpoly  47359  pgnbgreunbgrlem1  48611  pgnbgreunbgrlem4  48617  iooii  49415  icccldii  49416