Theorem adantrd 308

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

Hypothesis

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

Assertion

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

Proof of Theorem adantrd

Step	Hyp	Ref	Expression
1		adantrd.1	. 2 ⊢ (φ → (ψ → χ))
2		pm3.26 256	. 2 ⊢ ((ψ ∧ θ) → ψ)
3	1, 2	syl5 22	1 ⊢ (φ → ((ψ ∧ θ) → χ))

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  adantrr 312  consensus 574  2eu3 1069  zfaus 1480  unineq 1680  tz7.7 2224  oneqmini 2272  vtoclrbr 2450  fconstfv 2903  isomin 2937  isofrlem 2939  oecl 3140  oawordri 3152  unen 3338  mapenlem2 3385  pssnn 3428  cardinfima 3696  indpi 3828  1idpr 3927  prlem934a 3931  uzwo 4605  nnwoOLD 4608  qbtwnre 4650  ruclem13 4897  infxpidmlem8 4940  occllem6 5185  atom1d 5750  atexch 5769  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