Theorem adantrl 478

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  508  ad2ant2rl  511  3ad2antr2  1187  3ad2antr3  1188  xordidc  1441  foco  5558  fvun1  5699  isocnv  5934  isores2  5936  f1oiso2  5950  offval  6224  xp2nd  6310  1stconst  6365  2ndconst  6366  tfrlem9  6463  nnmordi  6660  dom2lem  6921  fundmen  6957  mapen  7003  ssenen  7008  ltsonq  7581  ltexnqq  7591  genprndl  7704  genprndu  7705  ltpopr  7778  ltsopr  7779  ltexprlemm  7783  ltexprlemopl  7784  ltexprlemopu  7786  ltexprlemdisj  7789  ltexprlemfl  7792  ltexprlemfu  7794  mulcmpblnrlemg  7923  cnegexlem2  8318  muladd  8526  eqord1  8626  eqord2  8627  divadddivap  8870  ltmul12a  9003  lemul12b  9004  cju  9104  zextlt  9535  supinfneg  9786  infsupneg  9787  xrre  10012  ixxdisj  10095  iooshf  10144  icodisj  10184  iccshftr  10186  iccshftl  10188  iccdil  10190  icccntr  10192  iccf1o  10196  fzaddel  10251  fzsubel  10252  seq3caopr  10712  seqcaoprg  10713  expineg2  10765  expsubap  10804  expnbnd  10880  facndiv  10956  hashfacen  11053  ccatpfx  11228  swrdccatfn  11251  swrdccatin2  11256  fprodeq0  12123  lcmdvds  12596  hashdvds  12738  eulerthlemh  12748  pceu  12813  pcqcl  12824  infpnlem1  12877  4sqlem11  12919  mhmpropd  13494  subsubm  13511  grplcan  13590  grplmulf1o  13602  dfgrp3mlem  13626  mulgfng  13656  mulgsubcl  13668  subsubg  13729  eqger  13756  resghm  13792  conjghm  13808  subsubrng  14172  subsubrg  14203  psrgrp  14643  txlm  14947  blininf  15092  xmeter  15104  xmetresbl  15108  limcimo  15333  dvdsppwf1o  15657  fsumdvdsmul  15659  sgmmul  15664