Theorem ad2ant2r 409

Description: Deduction adding two conjuncts to antecedent.

Hypothesis

Ref	Expression
ad2ant2.1	|- ((ph /\ ps) -> ch)

Assertion

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

Proof of Theorem ad2ant2r

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ((ph /\ ps) -> ch)
2	1	adantrr 395	. 2 |- ((ph /\ (ps /\ ta)) -> ch)
3	2	adantlr 393	1 |- (((ph /\ th) /\ (ps /\ ta)) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  foco 3682  omordi 4197  oaabs 4252  supmo 4576  genpnnp 5108  distrlem4pr 5130  ltexprlem7 5148  muladdt 5421  mulnzcnopr 5702  divmul13t 5782  divadddivt 5784  divdivdivt 5785  recdivt 5790  conjmult 5797  ltmul12it 5841  lemul12ait 5842  lemul12itOLD 5843  lediv12it 5896  lediv2it 5897  qrecclt 6273  iooint 6372  fzrevt 6511  lt2sqt 6630  le2sqt 6631  bernneq 6652  climge0 7112  climmullem3 7122  climmullem4 7123  climmullem5 7124  climcmpc1 7139  climsqueeze 7140  climsqueeze2 7141  climsup 7155  fsum0diaglem2 7257  mulc1cncf 7279  efaddlem11 7348  efaddlem13 7350  retopbas 7655  opnneissb 7728  ssblex 7856  metcnp 7887  tgioolem 7914  grprcan 8063  ablmul 8131  blocni 8465  ubthlem12 8540  ubthlem13 8541  spwpr3OLD 8662  hvsub4t 8906  chocuni 9172  shscl 9281  elspansn4t 9496  osumlem2 9579  osumlem3 9580  osumlem4 9581  5oalem2 9600  hosub4t 9739  hmopst 9945  hmopcot 9948  nmcopexlem5 9955  nmcopexlem6 9956  lnopcon 9963  nmcfnexlem5 9984  nmcfnexlem6 9985  lnfncon 9990  adjaddt 10026  hmopidmch 10079  hstpytht 10156  hstlest 10158  mdsl0 10237  mdslmd1lem2 10253  irredlem1 10317  irredlem2 10318  irredlem3 10319  irredlem4 10320  mdsymlem6 10335  cdj3lem2b 10364  eqidob 10723

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