Theorem anim12i 360

Description: Conjoin antecedents and consequents of two premises.

Hypotheses

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

Assertion

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

Proof of Theorem anim12i

Step	Hyp	Ref	Expression
1		simpl 346	. . 3 |- ((ph /\ ch) -> ph)
2		anim12i.1	. . 3 |- (ph -> ps)
3	1, 2	syl 12	. 2 |- ((ph /\ ch) -> ps)
4		simpr 350	. . 3 |- ((ph /\ ch) -> ch)
5		anim12i.2	. . 3 |- (ch -> th)
6	4, 5	syl 12	. 2 |- ((ph /\ ch) -> th)
7	3, 6	jca 310	1 |- ((ph /\ ch) -> (ps /\ th))

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  anim1i 361  anim2i 362  orim12i 363  pm5.18 722  orbidi 815  3anim123i 1053  sbimi 1537  mopick2OLD 1838  2exeu 1850  2mo 1851  cgsex2g 2322  cgsex4g 2323  cla42egv 2366  sseq1OLD 2638  sseq2 2639  uneqin 2845  uneqinOLD 2846  undif3 2854  ssunieq 3211  iuneq1 3269  iuneq2 3273  poeq2 3595  soeq2 3609  freq2 3633  tz7.7 3684  onfr 3702  eldifpw 3854  iunpw 3858  opbrop 4064  xpsspw 4093  cnveq 4135  dmeq 4157  xpexr2 4353  dfco2a 4394  funeq 4441  funeuOLD 4445  funun 4462  funprg 4466  funtp 4468  funinOLD 4485  2elresin 4524  funssxp 4577  fssres 4582  f1co 4612  dff1o2OLD 4640  f1ocnvOLD 4652  f1ores 4654  resdif 4659  f1oco 4661  fvreseq 4772  dff3 4790  exfo 4795  isocnv 4873  isotr 4874  isotrALT 4875  oprabval3 4959  ndmoprdistr 4982  ndmord 4983  tfrlem2 5120  tz7.49 5168  tz7.49c 5169  abianfp 5171  oaord 5228  oawordOLD 5231  omword 5249  omlimcl 5257  oen0 5261  oeword 5265  nnacom 5288  brecop 5365  brecop2 5366  ecopoprtrn 5370  th3qlem1 5373  th3q 5376  ixpeq2 5414  unen 5493  sbthlem8 5517  sbthlem9 5518  xpen 5582  mapenlem1 5583  xpmapenlem4 5593  mapunen 5596  isfinite1 5624  xpfi 5632  supmaxlem 5678  en2lp 5707  inf3lem3 5721  rankelun 5818  aceq5lem4 5900  kmlem16 5942  zorn2lem6 5955  brdom3 5963  brdom5 5964  brdom4 5965  unxpdom 5996  alephfp 6048  cdaval 6067  addcmpblnq 6204  mulcmpblnq 6205  ordpipq 6208  mulclpq 6212  mulasspq 6217  distrpqlem 6218  distrpq 6219  ltapq 6228  ltexpq 6232  halfpq 6234  genpn0 6258  genpnnp 6260  addclprlem2 6271  distrlem4pr 6282  prlem934 6291  ltapr 6303  addcmpblnr 6333  mulcmpblnr 6335  ltsrpr 6338  addclsr 6344  addasssr 6349  distrsr 6352  0idsr 6358  1idsr 6359  00sr 6360  mulgt0sr 6366  axaddopr 6417  axaddass 6430  axdistr 6432  cnegexlem3 6501  cnegex 6502  addsub4 6640  ltxrlt 6669  recextlem2 6875  divdivdivOLD 6962  ltmul2OLD 7010  lemul1OLD 7012  lemul2OLD 7014  lemul1aOLD 7020  lemul2aOLD 7022  lemul12aOLD 7025  lediv1OLD 7034  ltmuldiv2OLD 7048  ltdivmulOLD 7050  ledivmulOLD 7052  ledivmul2OLD 7057  lemuldiv2OLD 7060  lereci 7063  xrsupsslem 7285  xrinfmsslem 7286  supxrpnf 7297  zltp1le 7390  qaddcl 7449  qmulcl 7451  qreccl 7453  flmulnn0OLD 7509  iccneg 7576  elfzlem 7643  elfz2nn0 7667  fzsubel 7673  mulexp 7836  exprecOLD 7838  bernneqOLD 7899  digit1 7905  discrlem3 7908  sqabsadd 8099  sqabssub 8100  abs2dif 8154  cau5i 8171  faclbnd 8197  faclbnd3 8199  facavg 8207  fsumdivcALT 8296  clm3i 8339  climaddlem2 8375  climaddlem3 8376  climmullem3 8382  climmullem7 8386  climmullem8 8387  climcmplem 8397  climcji 8410  cvgratlem2 8513  fsum0diaglem2 8519  abscncflem 8536  cjcncf 8540  efaddlem5 8604  efaddlem6 8605  xpnnen 8768  ruclem28 8806  infxpidmlem11 8831  alephexp1 8853  tgcl 8894  uncld 8957  innei 9012  metreslem 9099  blss 9130  metcnconst 9163  metcnplem 9164  metcnpi3 9170  metcnpi4 9171  metcni2 9173  iscau5 9219  iscaunns 9222  lmsslem 9230  metelcls 9243  xplmi 9251  xplm 9253  xpcn 9254  oprcn 9255  bopcnlem2 9260  gxmul 9401  vcsub4 9527  nvaddsub4 9613  nvcni3 9663  vacnlem2 9668  vacnlem3 9669  vacnlem5 9671  lnosub 9759  blocni 9805  ubthlem8 9879  minveclem27 9916  minveclem28 9917  minveclem38 9927  htthlem6 9972  cdrci 10182  hvsub4 10538  occon2 10794  chocunii 10805  projlem26 10844  shscli 10914  shscom 10916  spanunsni 11135  spanpr 11136  hoscl 11156  hodcl 11158  osumlem1 11213  osumlem2 11214  osumlem4 11216  5oalem2 11235  5oalem3 11236  5oalem5 11238  3oalem1 11242  hoadddi 11366  hoadddir 11367  hosub4 11376  unopf1o 11477  counop 11482  lnophsi 11563  hmops 11582  hmopm 11583  nmophmi 11598  adjadd 11663  leop2 11695  leopadd 11703  leopmuli 11704  hmopidmchi 11723  pjclem4 11772  pj3si 11780  mdslmd1lem2 11898  mdslmd3i 11904  atomli 11954  atcvatlem 11957  irredlem3 11964  irredi 11966  atcvat3i 11968  mdsymlem1 11975  mdsymlem5 11979  cdjreui 12004  cdj3i 12013  addltmulALT 12018  bnj232 12075  bnj134 12478  bnj214 12508  bnj566 12544  bnj545 13271  bnj546 13272  bnj557 13281  bnj594 13300  bnj1001 13366  bnj1118 13420  bnj1398 13515  fseq1cl 13619  lediv2aALT 13621  ghomgrpilem2 13629  absdvdsb 13673  dvdsabsb 13674  muldvds1 13678  muldvds2 13679  dvdscmulr 13682  dvdsmulcr 13683  dvds2ln 13684  dvds2add 13685  dvds2sub 13686  divalglem9 13704  gcdcllem3 13720  gcdaddmlem 13734  gcdabs 13737  fresin 13840  tz6.26 13913  poxp 13949  poseq 13954  wfrlem5 13961  nocvxminlem 14028  axfelem12 14042  axfelem15 14045  axfelem16 14046  altxpsspw 14100  lukshef-ax2 14239  arg-ax 14240  nndivsub 14258  nndivlub 14259  elo 14342  ficli 14353  njtlc 14389  surrc2 14390  celsor 14443  valfunun 14460  ispr1 14496  isprj1 14505  cbicplem 14508  unprj 14511  ubos2 14598  ubos 14599  inposet 14620  tostos 14637  dfdir2 14639  dffprod 14670  gaplc 14731  curgrpact 14735  homcard 14893  topgele 14910  fgsb 14921  fgsb2 14925  altretop 14997  cntrsetlem 14999  mslb1 15007  2wsms 15008  iintlem1 15010  lvsovso 15038  dualcat2lem 15129  dualded2lem 15130  dualalg 15131  ismonc 15163  isepic 15173  fnctartar2 15285  uncomp 15433  connsub 15443  reconnlem3 15448  iccconn 15453  imaelfm 15591  difxp 15690  eropreu 15733  fzadd2 15791  fzsplit 15792  iserzshft2 15829  lincmb01cmp 15878  txmet 15925  heiborlem12 15966  phtpyco 16056  phtpcer 16062  isdivrng2 16111  divrngidl 16176  flddmn 16206  pridlc3 16221  pm10.14 16305  smores 16446  linepsub 17232  pmapsub 17250  elpaddri 17263  paddasslem14 17294  pmapjoin 17313

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain