Theorem anim12i 340

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

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  anim1i 341  anim2i 342  orim12i 343  orbidi 755  3anim123i 833  sbimi 1215  mopick2 1479  2exeu 1489  2mo 1490  cgsex2g 1879  cgsex4g 1880  cla42egv 1911  sseq1 2133  sseq2 2134  uneqin 2307  ssunieq 2585  iuneq1 2629  iuneq2 2632  poeq2 2899  soeq2 2910  eldifpw 2967  iunpw 2971  freq2 2980  tz7.7 3030  onfr 3043  opbrop 3295  xpsspw 3314  cnveq 3349  dmeq 3368  xpexr2 3537  funeq 3592  funeu 3594  funun 3611  funin 3623  2elresin 3655  funssxp 3695  fssres 3700  f1co 3724  f1o2 3750  f1ocnv 3758  f1ores 3760  f1oco 3764  fvreseq 3856  dff2 3874  exfo 3879  isocnv 3954  isotr 3955  isotrALT 3956  tfrlem2 3970  tz7.49 4017  tz7.49c 4018  abianfp 4020  oprabval3 4088  ndmoprdistr 4107  ndmord 4108  oaord 4239  oaword 4241  omword 4259  omlimcl 4267  oen0 4271  oeword 4275  nnacom 4291  brecop 4367  brecop2 4368  ecopoprtrn 4372  th3qlem1 4375  th3q 4378  ixpeq2 4416  unen 4497  sbthlem8 4517  sbthlem9 4518  xpen 4553  mapenlem1 4554  xpmapenlem4 4564  mapunen 4567  isfinite1 4595  supmaxlem 4648  en2lp 4664  inf3lem3 4677  rankelun 4769  aceq5lem4 4800  kmlem16 4842  zorn2lem6 4855  brdom3 4863  brdom5 4864  brdom4 4865  unxpdom 4909  alephfp 4965  cdaval 4984  addcmpblnq 5117  mulcmpblnq 5118  ordpipq 5121  mulclpq 5125  mulasspq 5130  distrpqlem 5131  distrpq 5132  ltapq 5141  ltexpq 5145  halfpq 5147  genpn0 5171  genpnnp 5173  addclprlem2 5184  distrlem4pr 5195  prlem934 5204  ltapr 5216  addcmpblnr 5246  mulcmpblnr 5248  ltsrpr 5251  addclsr 5257  addasssr 5262  distrsr 5265  0idsr 5271  1idsr 5272  00sr 5273  mulgt0sr 5279  axaddopr 5330  axaddass 5342  axdistr 5344  cnegexlem3 5412  cnegex 5413  addsub4 5538  ltxrlt 5565  recextlem2 5748  divcan5 5839  divdivdiv 5843  divdivmul 5853  lereci 5940  ltdiv23 5952  lediv23 5953  nndivtr 6021  xrsupsslem 6158  xrinfmsslem 6159  supxrpnf 6170  zltp1le 6263  qaddcl 6321  qmulcl 6323  qreccl 6325  iccneg 6433  elfzlem 6499  elfz2nn0 6521  fzsubel 6527  mulexp 6683  bernneq 6741  discrlem3 6748  sqabsadd 6938  sqabssub 6939  abs2dif 6992  cau5i 7009  faclbnd 7035  faclbnd3 7037  facavg 7045  fsumdivcALT 7126  clm3i 7169  climaddlem2 7205  climaddlem3 7206  climmullem3 7212  climmullem4 7213  climmullem7 7216  climmullem8 7217  climcmplem 7227  climcji 7240  cvgratlem2 7341  fsum0diaglem2 7347  abscncflem 7364  cjcncf 7368  efaddlem5 7432  efaddlem6 7433  xpnnen 7591  ruclem28 7629  infxpidmlem11 7654  alephexp1 7676  tgcl 7713  uncld 7766  innei 7821  metreslem 7907  blss 7938  metcnconst 7970  metcnplem 7971  metcnpi3 7977  metcnpi4 7978  metcni2 7980  iscau5 8026  iscaunns 8029  lmsslem 8037  metelcls 8050  xplmi 8058  xplm 8060  xpcn 8061  oprcn 8062  bopcnlem2 8067  vcsub4 8279  nvaddsub4 8365  nvcni3 8415  lnosub 8504  blocni 8549  ubthlem8 8620  minveclem27 8655  minveclem28 8656  minveclem38 8666  htthlem6 8709  eff1i 8827  hvsub4 8989  occon2 9244  chocunii 9255  projlem26 9294  shscli 9364  shscom 9366  spanunsni 9585  spanpr 9586  hoscl 9606  hodcl 9608  osumlem1 9661  osumlem2 9662  osumlem4 9664  5oalem2 9683  5oalem3 9684  5oalem5 9686  3oalem1 9690  hoadddi 9812  hoadddir 9813  hosub4 9822  unopf1o 9923  counop 9928  lnophsi 10009  hmops 10028  hmopm 10029  nmophmi 10044  adjadd 10109  leop2 10140  leopadd 10148  leopmuli 10149  hmopidmchi 10162  pjclem4 10211  pj3si 10219  mdslmd1lem2 10337  mdslmd3i 10343  atomli 10393  atcvatlem 10396  irredlem3 10403  irredi 10405  atcvat3i 10407  mdsymlem1 10414  mdsymlem5 10418  cdjreui 10443  cdj3i 10452  lediv2aALT 10456  ghomgrpilem2 10471  nndivsub 10508  nndivlub 10509  elo 10530  ficli 10553  inposet 10578  cdrci 10588  homcard 10633  fgsb 10663  fgsb2 10668  mslb1 10711  2wsms 10712  iintlem1 10714  ismonc 10824  isepic 10834

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 154  df-an 232

Copyright terms: Public domain