Theorem adantrl 482

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 110	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 286	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  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad2ant2l  512  ad2ant2rl  515  3ad2antr2  1194  3ad2antr3  1195  xordidc  1448  opabssxpd  4806  foco  5621  fvun1  5763  isocnv  6007  isores2  6009  f1oiso2  6023  offval  6300  xp2nd  6390  1stconst  6447  2ndconst  6448  tfrlem9  6580  nnmordi  6779  dom2lem  7048  fundmen  7084  mapen  7136  mapunen  7141  ssenen  7142  ltsonq  7755  ltexnqq  7765  genprndl  7878  genprndu  7879  ltpopr  7952  ltsopr  7953  ltexprlemm  7957  ltexprlemopl  7958  ltexprlemopu  7960  ltexprlemdisj  7963  ltexprlemfl  7966  ltexprlemfu  7968  mulcmpblnrlemg  8097  cnegexlem2  8492  muladd  8701  eqord1  8801  eqord2  8802  divadddivap  9047  ltmul12a  9180  lemul12b  9181  cju  9281  zextlt  9717  supinfneg  9974  infsupneg  9975  xrre  10201  ixxdisj  10284  iooshf  10333  icodisj  10373  iccshftr  10375  iccshftl  10377  iccdil  10379  icccntr  10381  iccf1o  10386  fzaddel  10443  fzsubel  10444  seq3caopr  10910  seqcaoprg  10911  expineg2  10963  expsubap  11002  expnbnd  11079  facndiv  11155  hashfibclem  11260  hashfacen  11262  hashf1lem1  11263  ccatpfx  11451  swrdccatfn  11474  swrdccatin2  11479  fprodeq0  12362  lcmdvds  12835  hashdvds  12977  eulerthlemh  12987  pceu  13052  pcqcl  13063  infpnlem1  13116  4sqlem11  13158  mhmpropd  13750  subsubm  13767  grplcan  13844  grplmulf1o  13856  dfgrp3mlem  13880  mulgfng  13904  mulgsubcl  13916  subsubg  13977  eqger  14004  resghm  14040  conjghm  14056  subsubrng  14495  subsubrg  14526  psrbagconf1o  14987  psrgrp  14999  txlm  15303  blininf  15448  xmeter  15460  xmetresbl  15464  limcimo  15689  dvdsppwf1o  16017  fsumdvdsmul  16019  sgmmul  16024  clwwlkn1loopb  16575