Theorem anim12d 566

Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)

Hypotheses

Ref	Expression
anim12d.1	|- ( ph -> ( ps -> ch ) )
anim12d.2	|- ( ph -> ( th -> ta ) )

Assertion

Ref	Expression
anim12d	|- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )

Proof of Theorem anim12d

Step	Hyp	Ref	Expression
1		anim12d.1	. 2 |- ( ph -> ( ps -> ch ) )
2		anim12d.2	. 2 |- ( ph -> ( th -> ta ) )
3		idd 26	. 2 |- ( ph -> ( ( ch /\ ta ) -> ( ch /\ ta ) ) )
4	1, 2, 3	syl2and 486	1 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )

Syntax hints:   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  anim1d  567  anim2d  568  prth  574  im2anan9  844  anim12dan  846  3anim123d  1343  mo3  2304  2euswap  2345  2moOLD  2349  ssunsn2  4158  disjiun  4413  soss  4791  wess  4839  frinxp  4918  trin2  5241  xp11  5290  ordtri3  5477  oneqmini  5492  funss  5618  fun  5762  fvcofneq  6044  dff13  6173  f1eqcocnv  6213  isores3  6240  isosolem  6252  isowe2  6255  ordom  6714  f1oweALT  6790  f1o2ndf1  6914  tposfn2  7005  tposf1o2  7009  wfrlem4  7049  smo11  7093  tz7.48lem  7168  om00  7286  omsmo  7365  ixpfi2  7880  elfiun  7952  supmo  7974  infmo  8019  alephord  8512  cardaleph  8526  dfac5  8565  fin1a2lem9  8844  axdc3lem2  8887  zorn2lem6  8937  grudomon  9248  indpi  9338  genpnmax  9438  reclem3pr  9480  reclem4pr  9481  suplem1pr  9483  supsrlem  9541  dedekind  9803  lemul12b  10468  fimaxre  10557  lbreu  10562  supadd  10581  supmullem2  10584  cju  10611  nnind  10633  uz11  11187  xrre2  11471  qbtwnre  11498  xrsupexmnf  11596  xrinfmexpnf  11597  ico0  11688  ioc0  11689  ssfzoulel  12010  ishashinf  12629  swrdccatin2  12843  coss12d  13034  sqrlem6  13309  o1lo1  13598  ruclem9  14287  isprm3  14630  eulerthlem2  14727  prmdiveq  14731  ramub2  14968  cictr  15707  joinfval  16244  meetfval  16258  clatl  16359  lubun  16366  ipodrsima  16408  dirtr  16479  mulgpropd  16788  dprdss  17659  subrgdvds  18019  dmatsubcl  19519  scmatcrng  19542  epttop  20020  cnpresti  20300  cnprest  20301  lmmo  20392  1stcrest  20464  lly1stc  20507  txcnp  20631  addcnlem  21892  caussi  22263  bcthlem5  22292  ovollb2lem  22437  voliunlem1  22499  ioombl1lem4  22510  rolle  22938  c1lip1  22945  c1lip3  22947  ulmval  23331  sqf11  24062  fsumvma  24137  dchrelbas3  24162  acopy  24870  brbtwn2  24931  axeuclidlem  24988  axcontlem9  24998  axcontlem10  24999  usgra2adedgspthlem1  25335  usgra2adedgwlkon  25339  usgra2wlkspthlem2  25344  constr3trllem2  25375  4cycl4v4e  25390  4cycl4dv  25391  usg2wlkonot  25607  usg2wotspth  25608  eupai  25691  2pthfrgrarn2  25734  frgranbnb  25744  subgoablo  26035  nmcvcn  26327  sspmval  26368  sspival  26373  sspimsval  26375  sspph  26492  shsubcl  26869  shorth  26944  5oalem6  27308  strlem1  27899  atexch  28030  cdj3i  28090  xrge0infssOLD  28345  xrofsup  28357  nnindf  28387  cnre2csqima  28723  erdszelem9  29928  erdsze2lem2  29933  ss2mcls  30212  funpsstri  30411  dfon2lem4  30437  dfon2  30443  trpredrec  30484  frmin  30485  wsuclem  30513  frrlem4  30522  nocvxminlem  30582  nocvxmin  30583  nofulllem5  30598  elfuns  30685  btwnswapid  30787  ifscgr  30814  hilbert1.2  30925  elicc3  30976  tailfb  31036  wl-mo3t  31867  ltflcei  31895  tan2h  31899  mblfinlem3  31941  fzmul  32031  metf1o  32046  ismtycnv  32096  ismtyres  32102  crngohomfo  32201  prtlem50  32385  hlhgt2  32921  hl2at  32937  2llnjN  33099  2lplnj  33152  linepsubN  33284  cdlemg33b0  34235  dvh3dim3N  34984  mapdh9a  35325  iocinico  36064  pm11.59  36647  infrglbOLD  37537  afvres  38434  usgvad2edg  39115  rhmsscrnghm  39420  ply1mulgsumlem1  39572  fldivexpfllog2  39770