Theorem mpanl12 714

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  spcimgfi1  3518  reuun1  4283  frminex  5631  tz6.26i  6339  wfii  6341  tfr2ALT  8376  tfr3ALT  8377  opthreg  9575  unsnen  10525  axcnre  11137  addgt0  11688  addgegt0  11689  addgtge0  11690  addge0  11691  addgt0i  11741  addge0i  11742  addgegt0i  11743  add20i  11745  mulge0i  11749  recextlem1  11832  recne0  11873  recdiv  11912  rec11i  11947  recgt1  12102  prodgt0i  12113  xadddi2  13314  iccshftri  13505  iccshftli  13507  iccdili  13509  icccntri  13511  mulexpz  14129  expaddz  14133  m1expeven  14136  iexpcyc  14234  cnpart  15281  resqrex  15291  sqreulem  15401  amgm2  15411  rlim  15536  ello12  15557  elo12  15568  bpolylem  16092  ege2le3  16134  dvdslelem  16357  divalglem1  16442  divalglem6  16446  divalglem9  16449  gcdaddmlem  16572  sqnprm  16751  prmlem1  17157  prmlem2  17170  m1expaddsub  19559  psgnuni  19560  gzrngunitlem  21542  lmres  23418  zdis  24935  iihalf1  25051  lmclimf  25424  vitali  25733  ismbf  25748  ismbfcn  25749  mbfconst  25753  cncombf  25778  cnmbf  25779  limcfval  25992  dvnfre  26072  quotlem  26422  ulmval  26501  ulmpm  26504  abelthlem2  26553  abelthlem3  26554  abelthlem5  26556  abelthlem7  26559  efcvx  26570  logtayl  26783  logccv  26786  cxpcn3  26871  emcllem2  27119  zetacvg  27137  basellem5  27207  bposlem7  27412  chebbnd1lem3  27593  dchrisumlem3  27613  iscgrgd  28740  axcontlem2  29224  nv1  30936  blocnilem  31065  ipasslem8  31098  siii  31114  ubthlem1  31131  norm1  31510  hhshsslem2  31529  hoscli  32023  hodcli  32024  cnlnadjlem7  32334  adjbdln  32344  pjnmopi  32409  strlem1  32511  rexdiv  33158  tpr2rico  34219  qqhre  34327  signsply0  34855  subfacval3  35552  erdszelem4  35557  erdszelem8  35561  elmrsubrn  35883  rdgprc  36155  fwddifval  36525  fwddifnval  36526  exrecfnlem  37885  poimirlem29  38160  ismblfin  38172  itg2addnclem  38182  caures  38271  sswfaxreg  45561  nthrucw  47460  cjnpoly  47481  pgnbgreunbgrlem1  48733  pgnbgreunbgrlem4  48739  iooii  49547  icccldii  49548