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  4236  suctr  4516  fvun1  5708  opabbrex  6060  poxp  6392  tposfo2  6428  1idprl  7800  1idpru  7801  uzind  9581  xrlttr  10020  fzen  10268  fz0fzelfz0  10352  ccatsymb  11169  fisumss  11943  fprodssdc  12141  zeqzmulgcd  12531  lcmgcdlem  12639  lcmdvds  12641  cncongr2  12666  exprmfct  12700  pceu  12858  infpnlem1  12922  isghm  13820  ringadd2  14030  metrest  15220  umgredg  15984  bj-charfunbi  16342  bj-om  16468