Theorem adantrd 279

Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)

Hypothesis

Ref	Expression
adantrd.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
adantrd	⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

Proof of Theorem adantrd

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adantrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 32	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem is referenced by:  syldan  282  jaoa  725  prlem1  979  equveli  1805  elssabg  4234  suctr  4514  fvun1  5706  opabbrex  6058  poxp  6390  tposfo2  6426  1idprl  7798  1idpru  7799  uzind  9579  xrlttr  10018  fzen  10266  fz0fzelfz0  10350  ccatsymb  11166  fisumss  11940  fprodssdc  12138  zeqzmulgcd  12528  lcmgcdlem  12636  lcmdvds  12638  cncongr2  12663  exprmfct  12697  pceu  12855  infpnlem1  12919  isghm  13817  ringadd2  14027  metrest  15217  umgredg  15980  bj-charfunbi  16316  bj-om  16442