Theorem adantld 390

Description: Deduction adding a conjunct to the left of an antecedent.

Hypothesis

Ref	Expression
adantld.1	|- (ph -> (ps -> ch))

Assertion

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

Proof of Theorem adantld

Step	Hyp	Ref	Expression
1		adantld.1	. . 3 |- (ph -> (ps -> ch))
2	1	a1d 12	. 2 |- (ph -> (th -> (ps -> ch)))
3	2	imp3a 361	1 |- (ph -> ((th /\ ps) -> ch))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  adantrl 394  dedlema 762  consensus 767  a4imed 1161  2eu3 1451  unineq 2255  tz7.7 2973  nnsuc 3148  tz7.49 3959  oaass 4195  omordi 4197  nnaordex 4249  xpdom2 4442  ensdomtr 4471  sdomen2 4482  mapenlem2 4490  inf3lem2 4614  trcl 4645  zorn2lem7 4794  cardaleph 4885  prlem934 5139  ltexprlem2 5143  ltexprlem7 5148  prlem936b 5154  suppsrlem 5221  suppsr2 5223  suppsr3 5224  suprelem 5259  xrlttrt 5553  supxrre 6083  dfuz 6202  uzindOLD 6208  sqr0 6672  bccl2t 6971  climmulc2 7129  expcnvlem6 7232  mulc1cncf 7279  acdcALT 7496  infpnlem1 7506  iscau3 7938  iscau4 7940  metelcls 7965  iscms2lem3 7991  cmsss 7997  bcthlem16 8014  bcthlem17 8015  chsscm 9112  mdsl2 10249  mdsl2b 10250  mdslmd1lem1 10252  atss 10273  chcv1t 10282  chrelat2 10292  atexcht 10308  cdj3lem1 10361  cmpassoh 10729

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