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 394

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 395

This theorem is referenced by:  reuun1  4317  frminex  5658  tz6.26i  6357  wfii  6360  wfr3OLD  8359  tfr2ALT  8422  tfr3ALT  8423  opthreg  9643  unsnen  10578  axcnre  11189  addgt0  11732  addgegt0  11733  addgtge0  11734  addge0  11735  addgt0i  11785  addge0i  11786  addgegt0i  11787  add20i  11789  mulge0i  11793  recextlem1  11876  recne0  11918  recdiv  11953  rec11i  11988  recgt1  12143  prodgt0i  12154  xadddi2  13311  iccshftri  13499  iccshftli  13501  iccdili  13503  icccntri  13505  mulexpz  14103  expaddz  14107  m1expeven  14110  iexpcyc  14206  cnpart  15223  resqrex  15233  sqreulem  15342  amgm2  15352  rlim  15475  ello12  15496  elo12  15507  bpolylem  16028  ege2le3  16070  dvdslelem  16289  divalglem1  16374  divalglem6  16378  divalglem9  16381  gcdaddmlem  16502  sqnprm  16676  prmlem1  17080  prmlem2  17092  m1expaddsub  19465  psgnuni  19466  gzrngunitlem  21382  lmres  23248  zdis  24776  iihalf1  24896  lmclimf  25276  vitali  25586  ismbf  25601  ismbfcn  25602  mbfconst  25606  cncombf  25631  cnmbf  25632  limcfval  25845  dvnfre  25928  quotlem  26280  ulmval  26361  ulmpm  26364  abelthlem2  26414  abelthlem3  26415  abelthlem5  26417  abelthlem7  26420  efcvx  26431  logtayl  26639  logccv  26642  cxpcn3  26728  emcllem2  26974  zetacvg  26992  basellem5  27062  bposlem7  27268  chebbnd1lem3  27449  dchrisumlem3  27469  iscgrgd  28389  axcontlem2  28848  nv1  30557  blocnilem  30686  ipasslem8  30719  siii  30735  ubthlem1  30752  norm1  31131  hhshsslem2  31150  hoscli  31644  hodcli  31645  cnlnadjlem7  31955  adjbdln  31965  pjnmopi  32030  strlem1  32132  rexdiv  32734  tpr2rico  33644  qqhre  33752  signsply0  34314  subfacval3  34930  erdszelem4  34935  erdszelem8  34939  elmrsubrn  35261  rdgprc  35521  fwddifval  35889  fwddifnval  35890  exrecfnlem  36989  poimirlem29  37253  ismblfin  37265  itg2addnclem  37275  caures  37364  iooii  48122  icccldii  48123