Theorem adantrl 311

Description: Deduction adding a conjunct to an antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem adantrl

Step	Hyp	Ref	Expression
1		adant2.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	exp 291	. . 3 |- (ph -> (ps -> ch))
3	2	adantld 307	. 2 |- (ph -> ((th /\ ps) -> ch))
4	3	imp 277	1 |- ((ph /\ (th /\ ps)) -> ch)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  anabss3 382  sbcom 916  supmo 2156  ordelord 2221  ordsucun 2333  f1oco 2816  f1ocnvfvb 2922  isocnv 2934  isotr 2935  isotrALT 2936  tfrlem8 2956  tfrlem9 2957  tfrlem11 2959  caoprmo 3084  oaass 3163  omordi 3164  dom2d 3307  fundmen 3333  xpdom2 3345  sbthlem9 3357  mapenlem2 3385  mapunen 3397  ssenen 3399  inf3lem6 3469  axacndlem4 3756  axacndlem5 3757  axacnd 3758  ltsopq 3869  ltapq 3870  ltmpq 3871  ltexpq 3874  prlem936a 3947  mulcmpblnr 3977  ltsosr 3997  ssgt0sr 4011  divmuldivt 4263  divadddivt 4264  divdivdivt 4265  divdiv23t 4271  zltp1let 4597  zmax 4618  qaddclt 4642  qbtwnre 4650  infxpidmlem7 4939  infxpidmlem11 4943  hvsub4t 5014  chocuni 5179  osumlem3 5532  osumlem4 5533  spansncv 5542  5oalem2 5545  3oalem2 5553  ssmd2 5735  chrelat2 5758  atcvatlem 5770  atcvat 5771  atcvat3 5774  atcvat4 5775  mdsymlem1 5776  mdsymlem3 5778  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