HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem anim12d 556
Description: Conjoin antecedents and consequents in a deduction.
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
StepHypRef Expression
1 prth 554 . 2 |- (((ps -> ch) /\ (th -> ta)) -> ((ps /\ th) -> (ch /\ ta)))
2 anim12d.1 . 2 |- (ph -> (ps -> ch))
3 anim12d.2 . 2 |- (ph -> (th -> ta))
41, 2, 3sylanc 471 1 |- (ph -> ((ps /\ th) -> (ch /\ ta)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  anim12ii 557  anim1d 558  anim2d 559  im2anan9 561  im2anan9r 562  pm5.74 581  pm5.18 658  3anim123d 897  hband 1107  hbbid 1108  2euswap 1438  exists2 1451  soss 2843  sotrieq 2852  wess 2926  ordtri3 2973  oneqmini 3007  ordunel 3074  weinxp 3223  xp11 3463  fun 3626  f1fv 3859  isotr 3882  isotrALT 3883  f1oweALT 3891  tfrlem1 3896  tz7.48lem 3940  om00 4190  omsmo 4241  ensdomtr 4451  domsdomtr 4456  aceq5 4712  zorn2lem6 4765  unidom 4780  alephord 4847  cardaleph 4857  indpi 5006  genpnmax 5082  reclem3pr 5130  reclem4pr 5131  suplem1pr 5133  suppsr2 5195  suppsr3 5196  pre-axsup 5263  xrre2t 5543  lemul12ait 5798  nnind 5885  lbreu 5992  xrsupexmnf 6021  xrinfmexpnf 6022  elnn0nn 6118  uzwo5OLD 6159  qbtwnre 6216  elioc2t 6322  elico2t 6323  elicc2t 6324  ioossicc 6330  uz11t 6364  sqrlem5 6607  replimt 6692  caubnd 6863  climaddlem3 7052  climmullem8 7063  caucvglem2 7094  rescncf 7207  infmap2lem2 7522  basgen2t 7581  opnin 7809  metcnss2 7838  cncfmet 7844  caussi 7889  iscms2lem4 7926  grplactf1o 8034  subgabl 8060  sspmval 8326  sspival 8331  sspimsval 8333  sspph 8446  pslem 8573  shsubclt 9010  shsubcltOLD 9011  shorth 9084  occllem7 9095  projlem27 9128  osumlem4 9498  5oalem6 9521  strlem1 10087  atexcht 10216  cdj3 10273  uninqs 10342  oooeqim2 10371  cnrsfin 10396  cnrscoa 10397  cmphmp 10408  homcard 10426  filintf 10443  trnij 10481  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