Theorem ad2ant2r 418

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 404	. 2 |- ((ph /\ (ps /\ ta)) -> ch)
3	2	adantlr 402	1 |- (((ph /\ th) /\ (ps /\ ta)) -> ch)

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  foco 3739  omordi 4255  oaabs 4310  supmo 4636  genpnnp 5173  distrlem4pr 5195  ltexprlem7 5213  muladd 5486  mulnzcnopr 5767  divmul13 5840  divadddiv 5842  divdivdiv 5843  recdiv 5848  conjmul 5855  ltmul12a 5899  lemul12b 5900  lemul12aOLD 5901  lediv12a 5956  lediv2a 5957  qreccl 6325  irrmul 6330  iooin 6397  fzrev 6537  lt2sq 6719  le2sq 6720  bernneq 6741  climge0 7202  climmullem3 7212  climmullem4 7213  climmullem5 7214  climcmpc1 7229  climsqueeze 7230  climsqueeze2 7231  climsupi 7245  fsum0diaglem2 7347  mulc1cncf 7369  efaddlem11 7438  efaddlem13 7440  retopbas 7740  opnneissb 7813  ssblex 7941  metcnp 7972  tgioolem 7999  grprcan 8147  ablmul 8215  blocni 8549  ubthlem12 8624  ubthlem13 8625  hvsub4 8989  chocunii 9255  shscli 9364  elspansn4 9579  osumlem2 9662  osumlem3 9663  osumlem4 9664  5oalem2 9683  hosub4 9822  hmops 10028  hmopco 10031  nmcopexlem5 10038  nmcopexlem6 10039  lnopconi 10046  nmcfnexlem5 10067  nmcfnexlem6 10068  lnfnconi 10073  adjadd 10109  hmopidmchi 10162  hstpyth 10240  hstles 10242  mdsl0 10321  mdslmd1lem2 10337  irredlem1 10401  irredlem2 10402  irredlem3 10403  irredlem4 10404  mdsymlem6 10419  cdj3lem2b 10448  eqidob 10805

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