Theorem anim12i 333

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		pm3.26 319	. . 3 |- ((ph /\ ch) -> ph)
2		anim12i.1	. . 3 |- (ph -> ps)
3	1, 2	syl 10	. 2 |- ((ph /\ ch) -> ps)
4		pm3.27 323	. . 3 |- ((ph /\ ch) -> ch)
5		anim12i.2	. . 3 |- (ch -> th)
6	4, 5	syl 10	. 2 |- ((ph /\ ch) -> th)
7	3, 6	jca 288	1 |- ((ph /\ ch) -> (ps /\ th))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  anim1i 334  anim2i 335  orim12i 336  orbidi 741  3anim123i 819  sbimi 1169  mopick2 1429  2exeu 1439  2mo 1440  cgsex2g 1823  cgsex4g 1824  cla42egv 1855  sseq1 2072  sseq2 2073  uneqin 2246  ssunieq 2521  iuneq1 2565  iuneq2 2568  poeq2 2834  soeq2 2845  eldifpw 2900  iunpw 2904  freq2 2913  tz7.7 2963  onfr 2976  opbrop 3228  xpsspw 3247  cnveq 3281  dmeq 3300  xpexr2 3466  funeq 3521  funeu 3523  funun 3540  funin 3552  2elresin 3584  funssxp 3623  fssres 3628  f1co 3652  f1o2 3678  f1ocnv 3686  f1ores 3688  f1oco 3692  fvreseq 3784  dff2 3802  exfo 3807  isocnv 3881  isotr 3882  isotrALT 3883  tfrlem2 3897  tz7.49 3944  tz7.49c 3945  abianfp 3947  oprabval3 4015  ndmoprdistr 4035  ndmord 4036  oaord 4165  oaword 4167  omword 4185  omlimcl 4193  oen0 4197  oeword 4201  nnacom 4217  brecop 4290  brecop2 4291  ecopoprtrn 4295  th3qlem1 4298  th3q 4301  ixpeq2 4339  unen 4414  sbthlem8 4434  sbthlem9 4435  xpen 4468  mapenlem1 4469  xpmapenlem4 4479  mapunen 4482  isfinite1 4510  en2lp 4574  inf3lem3 4587  rankelun 4679  aceq5lem4 4710  kmlem16 4752  zorn2lem6 4765  brdom3 4773  brdom5 4774  brdom4 4775  unxpdom 4816  alephfp 4872  cdavalt 4891  addcmpblnq 5024  mulcmpblnq 5025  ordpipq 5028  mulclpq 5032  mulasspq 5037  distrpqlem 5038  distrpq 5039  ltapq 5048  ltexpq 5052  halfpq 5054  genpn0 5078  genpnnp 5080  addclprlem2 5091  distrlem4pr 5102  prlem934 5111  ltapr 5123  addcmpblnr 5153  mulcmpblnr 5155  ltsrpr 5158  addclsr 5164  addasssr 5169  distrsr 5172  0idsr 5178  1idsr 5179  00sr 5180  mulgt0sr 5186  axaddopr 5237  axaddass 5249  axdistr 5251  cnegextlem3 5319  cnegext 5320  addsub4t 5445  ltxrltt 5472  recextlem2 5656  divcan5t 5737  divdivdivt 5741  divdivmult 5751  lerec 5828  ltdiv23t 5840  lediv23t 5841  nndivtrt 5907  xrsupsslem 6023  xrinfmsslem 6024  supxrpnf 6035  zltp1let 6128  qaddclt 6207  qmulclt 6209  qrecclt 6211  qdivclt 6212  ioonegt 6339  iccnegt 6340  elfzlem 6405  elfz2nn0t 6427  fzsubelt 6433  mulexpt 6525  bernneq 6583  discrlem3 6588  sqabsaddt 6783  sqabssubt 6784  abs2dift 6839  cau5 6856  faclbnd 6882  faclbnd3 6884  facavgt 6892  fsumdivcALT 6974  clm3 7017  climaddlem2 7051  climaddlem3 7052  climmullem3 7058  climmullem4 7059  climmullem7 7062  climmullem8 7063  climcmplem 7073  climcj 7086  cvgratlem2 7186  fsum0diaglem2 7192  abscncflem 7209  cjcncf 7213  efaddlem5 7284  efaddlem6 7285  xpnnen 7441  ruclem28 7480  infxpidmlem11 7505  alephexp1 7526  tgclt 7566  uncld 7623  innei 7677  metreslem 7762  blss 7793  metcnconst 7824  metcnplem 7825  metcnpi3 7831  metcnpi4 7832  metcni2 7834  iscau5 7878  lmsslem 7887  metelcls 7900  xplmi 7907  xplm 7909  xpcn 7910  oprcn 7911  bopcnlem2 7916  vcsub4 8132  nvaddsub4 8221  lnosub 8353  blocni 8396  ubthlem8 8467  minveclem27 8502  minveclem28 8503  minveclem38 8513  htthlem6 8555  circcltOLD 8656  eff1i 8665  hvsub4t 8827  occon2t 9077  chocuni 9088  projlem26 9127  shscl 9196  shscomt 9198  spanunsn 9419  spanpr 9420  hosclt 9440  hodclt 9442  osumlem1 9495  osumlem2 9496  osumlem4 9498  5oalem2 9517  5oalem3 9518  5oalem5 9520  3oalem1 9524  hoadddit 9646  hoadddirt 9647  hosub4t 9656  unopf1ot 9756  counopt 9761  lnophs 9841  hmopst 9860  hmopmt 9861  nmophm 9876  adjaddt 9940  leop2t 9969  leopaddt 9977  leopmulit 9978  hmopidmch 9990  pjclem4 10037  pj3s 10045  mdslmd1lem2 10161  mdslmd3 10167  atoml 10217  atcvatlem 10220  irredlem3 10227  irred 10229  atcvat3 10231  mdsymlem1 10238  mdsymlem5 10242  cdjreu 10264  cdj3 10273  lediv2itALT 10276  ghomgrpilem2 10291  elo 10345  ficli 10368  cdrci 10381  homcard 10426  fgsb 10444  fgsb2 10449  mslb1 10473  2wsms 10474  iintlem1 10476  ismonc 10584

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 147  df-an 225

Copyright terms: Public domain