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 3673  omordi 4187  oaabs 4242  supmo 4556  genpnnp 5088  distrlem4pr 5110  ltexprlem7 5128  muladdt 5401  mulnzcnopr 5679  divmul13t 5746  divadddivt 5748  divdivdivt 5749  recdivt 5754  conjmult 5761  ltmul12it 5805  lemul12ait 5806  lemul12itOLD 5807  lediv12it 5852  lediv2it 5853  qrecclt 6219  iooint 6317  fzrevt 6451  lt2sqt 6569  le2sqt 6570  bernneq 6591  climge0 7057  climmullem3 7066  climmullem4 7067  climmullem5 7068  climcmpc1 7083  climsqueeze 7084  climsqueeze2 7085  climsup 7099  fsum0diaglem2 7200  mulc1cncf 7222  efaddlem11 7298  efaddlem13 7300  retopbas 7605  opnneissb 7678  ssblex 7808  metcnp 7839  tgioolem 7866  grprcan 8013  ablmul 8083  blocni 8409  ubthlem12 8484  ubthlem13 8485  hvsub4t 8845  chocuni 9111  shscl 9219  elspansn4t 9436  osumlem2 9519  osumlem3 9520  osumlem4 9521  5oalem2 9540  hosub4t 9679  hmopst 9883  hmopcot 9886  nmcopexlem5 9893  nmcopexlem6 9894  lnopcon 9901  nmcfnexlem5 9922  nmcfnexlem6 9923  lnfncon 9928  adjaddt 9964  hmopidmch 10017  hstpytht 10094  hstlest 10096  mdsl0 10174  mdslmd1lem2 10190  irredlem1 10254  irredlem2 10255  irredlem3 10256  irredlem4 10257  mdsymlem6 10272  cdj3lem2b 10298  eqidob 10603

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