Theorem anim12d 563

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 24	. 2 |- ( ph -> ( ( ch /\ ta ) -> ( ch /\ ta ) ) )
4	1, 2, 3	syl2and 483	1 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ ta ) ) )

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  anim1d  564  anim2d  565  prth  571  im2anan9  833  anim12dan  835  3anim123d  1306  mo3  2320  2euswap  2379  2moOLD  2383  ssunsn2  4186  disjiun  4437  soss  4818  wess  4866  ordtri3  4914  oneqmini  4929  frinxp  5064  trin2  5389  xp11  5441  funss  5605  fun  5747  fvcofneq  6028  dff13  6153  f1eqcocnv  6191  isores3  6218  isosolem  6230  isowe2  6233  ordom  6688  f1oweALT  6768  f1o2ndf1  6891  tposfn2  6977  tposf1o2  6981  smo11  7035  tz7.48lem  7106  om00  7224  omsmo  7303  ixpfi2  7817  elfiun  7889  supmo  7911  alephord  8455  cardaleph  8469  dfac5  8508  fin1a2lem9  8787  axdc3lem2  8830  zorn2lem6  8880  grudomon  9194  indpi  9284  genpnmax  9384  reclem3pr  9426  reclem4pr  9427  suplem1pr  9429  supsrlem  9487  dedekind  9742  lemul12b  10398  fimaxre  10489  lbreu  10492  supmullem2  10509  cju  10531  nnind  10553  uz11  11103  xrre2  11370  qbtwnre  11397  xrsupexmnf  11495  xrinfmexpnf  11496  ico0  11574  ioc0  11575  ssfzoulel  11873  swrdnd  12619  swrdccatin2  12674  sqrlem6  13043  o1lo1  13322  ruclem9  13831  isprm3  14084  eulerthlem2  14170  prmdiveq  14174  ramub2  14390  joinfval  15487  meetfval  15501  clatl  15602  lubun  15609  ipodrsima  15651  dirtr  15722  mulgpropd  15982  dprdss  16875  subrgdvds  17238  dmatsubcl  18783  scmatcrng  18806  epttop  19292  cnpresti  19571  cnprest  19572  lmmo  19663  1stcrest  19736  lly1stc  19779  txcnp  19872  addcnlem  21119  caussi  21487  bcthlem5  21518  ovollb2lem  21650  voliunlem1  21711  ioombl1lem4  21722  rolle  22142  c1lip1  22149  c1lip3  22151  ulmval  22525  sqf11  23157  fsumvma  23232  dchrelbas3  23257  brbtwn2  23900  axeuclidlem  23957  axcontlem9  23967  axcontlem10  23968  usgra2adedgspthlem1  24303  usgra2adedgwlkon  24307  usgra2wlkspthlem2  24312  constr3trllem2  24343  4cycl4v4e  24358  4cycl4dv  24359  usg2wlkonot  24575  usg2wotspth  24576  eupai  24659  2pthfrgrarn2  24702  frgranbnb  24712  subgoablo  25005  nmcvcn  25297  sspmval  25338  sspival  25343  sspimsval  25345  sspph  25462  shsubcl  25830  shorth  25905  5oalem6  26269  strlem1  26861  atexch  26992  cdj3i  27052  xrge0infss  27264  xrofsup  27266  ishashinf  27290  nnindf  27294  cnre2csqima  27545  erdszelem9  28299  erdsze2lem2  28304  funpsstri  28788  dfon2lem4  28811  dfon2  28817  trpredrec  28914  frmin  28915  wfrlem4  28939  wsuclem  28974  frrlem4  28983  nocvxminlem  29043  nocvxmin  29044  nofulllem5  29059  elfuns  29158  btwnswapid  29260  ifscgr  29287  hilbert1.2  29398  wl-mo3t  29614  supadd  29635  ltflcei  29636  tan2h  29640  mblfinlem3  29646  elicc3  29728  tailfb  29814  fzmul  29852  metf1o  29867  ismtycnv  29917  ismtyres  29923  crngohomfo  30022  prtlem50  30208  iocinico  30800  pm11.59  30891  infrglb  31156  afvres  31740  usgvad2edg  31894  ply1mulgsumlem1  32076  hlhgt2  34194  hl2at  34210  2llnjN  34372  2lplnj  34425  linepsubN  34557  cdlemg33b0  35506  dvh3dim3N  36255  mapdh9a  36596  coss12d  36788  bj-frege52a  36877