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  4231  suctr  4511  fvun1  5699  opabbrex  6047  poxp  6376  tposfo2  6411  1idprl  7773  1idpru  7774  uzind  9554  xrlttr  9987  fzen  10235  fz0fzelfz0  10319  ccatsymb  11132  fisumss  11898  fprodssdc  12096  zeqzmulgcd  12486  lcmgcdlem  12594  lcmdvds  12596  cncongr2  12621  exprmfct  12655  pceu  12813  infpnlem1  12877  isghm  13775  ringadd2  13985  metrest  15174  umgredg  15937  bj-charfunbi  16132  bj-om  16258