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  4232  suctr  4512  fvun1  5702  opabbrex  6054  poxp  6384  tposfo2  6419  1idprl  7788  1idpru  7789  uzind  9569  xrlttr  10003  fzen  10251  fz0fzelfz0  10335  ccatsymb  11150  fisumss  11918  fprodssdc  12116  zeqzmulgcd  12506  lcmgcdlem  12614  lcmdvds  12616  cncongr2  12641  exprmfct  12675  pceu  12833  infpnlem1  12897  isghm  13795  ringadd2  14005  metrest  15195  umgredg  15958  bj-charfunbi  16229  bj-om  16355