Theorem anim12i 268

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 256	. . 3 |- ((ph /\ ch) -> ph)
2		anim12i.1	. . 3 |- (ph -> ps)
3	1, 2	syl 12	. 2 |- ((ph /\ ch) -> ps)
4		pm3.27 260	. . 3 |- ((ph /\ ch) -> ch)
5		anim12i.2	. . 3 |- (ch -> th)
6	4, 5	syl 12	. 2 |- ((ph /\ ch) -> th)
7	3, 6	jca 236	1 |- ((ph /\ ch) -> (ps /\ th))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  anim1i 269  anim2i 270  orim12i 271  orbidi 510  im3an 605  sbimi 854  mopick2 1057  2exeu 1066  cgsex2g 1368  cgsex4g 1369  cla4e2gv 1398  sseq1 1521  sseq2 1522  ssunieq 1945  iuneq1 2003  iuneq2 2006  iunpw 2040  opelopabg 2115  poeq2 2131  soeq2 2142  freq2 2175  tz7.2 2183  tz7.7 2224  onfr 2237  opbrop 2472  xpex 2488  cnveq 2513  dmeq 2531  coexg 2671  funeq 2683  funeu 2685  funun 2700  funin 2708  2elresin 2733  fssres 2764  f1co 2783  f1o2 2804  f1ocnv 2811  f1ores 2813  f1oco 2816  fvreseq 2882  isotr 2935  isotrALT 2936  tfrlem2 2950  tz7.49 2997  tz7.49c 2998  abianfp 3000  oprabval3 3052  ndmoprdistr 3063  ndmord 3064  oaord 3149  oaword 3151  oen0 3165  nnacom 3175  nnmord 3189  brecop 3242  brecop2 3243  ecopoprtrn 3247  th3qlem1 3250  th3q 3253  unen 3338  sbthlem8 3356  sbthlem9 3357  xpen 3383  xpmapenlem4 3394  mapunen 3397  isfinite1 3425  en2lp 3453  inf3lem3 3466  aceq5lem4 3561  kmlem16 3595  zornlem6 3608  unxpdom 3650  cdavalt 3716  addcmpblnq 3846  mulcmpblnq 3847  ordpipq 3850  mulclpq 3854  mulasspq 3859  distrpqlem 3860  distrpq 3861  ltapq 3870  ltexpq 3874  halfpq 3876  genpn0 3900  genpnnp 3902  addclprlem2 3913  distrlem4pr 3924  prlem934 3933  ltapr 3945  addcmpblnr 3975  mulcmpblnr 3977  ltsrpr 3980  addclsr 3986  addasssr 3991  distrsr 3994  0idsr 4000  1idsr 4001  00sr 4002  mulgt0sr 4008  axaddcl 4066  axaddass 4072  axdistr 4074  axnegex 4078  axrecex 4079  divdivdivt 4265  lerec 4411  zltp1let 4597  qaddclt 4642  qmulclt 4644  qrecclt 4646  qdivclt 4647  discrlem3 4715  ruclem28 4912  xpnnen 4927  infxpidmlem11 4943  alephexp1 4954  hvsub4t 5014  occon2t 5169  chocuni 5179  projlem2 5194  projlem26 5218  shscl 5282  shscomt 5284  spanunsn 5482  hosclt 5491  hodclt 5492  osumlem1 5530  osumlem2 5531  osumlem3 5532  osumlem4 5533  5oalem2 5545  5oalem3 5546  5oalem5 5548  3oalem1 5552  pjclem4 5653  pj3s 5659  atcvatlem 5770  atcvat3 5774  mdsymlem1 5776  mdsymlem5 5780

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org