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  1190  3ad2antr3  1191  xordidc  1444  opabssxpd  4791  foco  5606  fvun1  5748  isocnv  5990  isores2  5992  f1oiso2  6006  offval  6283  xp2nd  6373  1stconst  6430  2ndconst  6431  tfrlem9  6563  nnmordi  6762  dom2lem  7024  fundmen  7060  mapen  7112  mapunen  7117  ssenen  7118  ltsonq  7729  ltexnqq  7739  genprndl  7852  genprndu  7853  ltpopr  7926  ltsopr  7927  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemdisj  7937  ltexprlemfl  7940  ltexprlemfu  7942  mulcmpblnrlemg  8071  cnegexlem2  8465  muladd  8674  eqord1  8774  eqord2  8775  divadddivap  9018  ltmul12a  9151  lemul12b  9152  cju  9252  zextlt  9688  supinfneg  9945  infsupneg  9946  xrre  10172  ixxdisj  10255  iooshf  10304  icodisj  10344  iccshftr  10346  iccshftl  10348  iccdil  10350  icccntr  10352  iccf1o  10357  fzaddel  10414  fzsubel  10415  seq3caopr  10881  seqcaoprg  10882  expineg2  10934  expsubap  10973  expnbnd  11050  facndiv  11126  hashfibclem  11231  hashfacen  11233  ccatpfx  11418  swrdccatfn  11441  swrdccatin2  11446  fprodeq0  12328  lcmdvds  12801  hashdvds  12943  eulerthlemh  12953  pceu  13018  pcqcl  13029  infpnlem1  13082  4sqlem11  13124  mhmpropd  13721  subsubm  13738  grplcan  13817  grplmulf1o  13829  dfgrp3mlem  13853  mulgfng  13877  mulgsubcl  13889  subsubg  13950  eqger  13977  resghm  14013  conjghm  14029  subsubrng  14460  subsubrg  14491  psrbagconf1o  14954  psrgrp  14966  txlm  15270  blininf  15415  xmeter  15427  xmetresbl  15431  limcimo  15656  dvdsppwf1o  15983  fsumdvdsmul  15985  sgmmul  15990  clwwlkn1loopb  16541