Theorem adantld 307

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

Hypothesis

Ref	Expression
adantld.1	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
adantld	⊢ (φ → ((θ ∧ ψ) → χ))

Proof of Theorem adantld

Step	Hyp	Ref	Expression
1		adantld.1	. . 3 ⊢ (φ → (ψ → χ))
2	1	a1d 14	. 2 ⊢ (φ → (θ → (ψ → χ)))
3	2	imp3a 279	1 ⊢ (φ → ((θ ∧ ψ) → χ))

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  adantrl 311  dedlema 569  consensus 574  a4c1 844  2eu3 1069  unineq 1680  tz7.7 2224  nnsuc 2389  oaass 3163  omordi 3164  nnaordex 3191  xpdom2 3345  ensdomtr 3372  sdomen2 3380  mapenlem2 3385  inf3lem2 3465  trcl 3489  zornlem7 3609  cardaleph 3690  prlem934 3933  ltexprlem2 3937  ltexprlem7 3942  prlem936b 3948  suppsrlem 4015  suppsr2 4017  suppsr3 4018  suprelem 4053  uzind 4603  sqr0 4730  chsscm 5147  chcv1t 5751  chrelat2 5758  atexch 5769

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