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  728  prlem1  982  equveli  1807  elssabg  4243  suctr  4524  fvun1  5721  opabbrex  6075  poxp  6406  tposfo2  6476  1idprl  7853  1idpru  7854  uzind  9635  xrlttr  10074  fzen  10323  fz0fzelfz0  10407  ccatsymb  11228  fisumss  12016  fprodssdc  12214  zeqzmulgcd  12604  lcmgcdlem  12712  lcmdvds  12714  cncongr2  12739  exprmfct  12773  pceu  12931  infpnlem1  12995  isghm  13893  ringadd2  14104  metrest  15300  umgredg  16069  bj-charfunbi  16510  bj-om  16636