Theorem adantrl 467

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantrl	⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

Proof of Theorem adantrl

Step	Hyp	Ref	Expression
1		simpr 109	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 282	1 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad2ant2l  497  ad2ant2rl  500  3ad2antr2  1128  3ad2antr3  1129  xordidc  1358  foco  5311  fvun1  5439  isocnv  5664  isores2  5666  f1oiso2  5680  offval  5941  xp2nd  6016  1stconst  6070  2ndconst  6071  tfrlem9  6168  nnmordi  6364  dom2lem  6618  fundmen  6652  mapen  6691  ssenen  6696  ltsonq  7148  ltexnqq  7158  genprndl  7271  genprndu  7272  ltpopr  7345  ltsopr  7346  ltexprlemm  7350  ltexprlemopl  7351  ltexprlemopu  7353  ltexprlemdisj  7356  ltexprlemfl  7359  ltexprlemfu  7361  mulcmpblnrlemg  7477  cnegexlem2  7855  muladd  8059  eqord1  8158  eqord2  8159  divadddivap  8394  ltmul12a  8522  lemul12b  8523  cju  8623  zextlt  9041  supinfneg  9286  infsupneg  9287  xrre  9490  ixxdisj  9573  iooshf  9622  icodisj  9662  iccshftr  9664  iccshftl  9666  iccdil  9668  icccntr  9670  iccf1o  9674  fzaddel  9726  fzsubel  9727  seq3caopr  10143  expineg2  10189  expsubap  10228  expnbnd  10302  facndiv  10372  hashfacen  10466  lcmdvds  11600  hashdvds  11736  txlm  12284  blininf  12407  xmeter  12419  xmetresbl  12423  limcimo  12584