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  721  prlem1  975  equveli  1773  elssabg  4182  suctr  4457  fvun1  5630  opabbrex  5970  poxp  6299  tposfo2  6334  1idprl  7676  1idpru  7677  uzind  9456  xrlttr  9889  fzen  10137  fz0fzelfz0  10221  fisumss  11576  fprodssdc  11774  zeqzmulgcd  12164  lcmgcdlem  12272  lcmdvds  12274  cncongr2  12299  exprmfct  12333  pceu  12491  infpnlem1  12555  isghm  13451  ringadd2  13661  metrest  14850  bj-charfunbi  15565  bj-om  15691