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  1189  3ad2antr3  1190  xordidc  1443  opabssxpd  4762  foco  5570  fvun1  5712  isocnv  5951  isores2  5953  f1oiso2  5967  offval  6242  xp2nd  6328  1stconst  6385  2ndconst  6386  tfrlem9  6484  nnmordi  6683  dom2lem  6944  fundmen  6980  mapen  7031  ssenen  7036  ltsonq  7617  ltexnqq  7627  genprndl  7740  genprndu  7741  ltpopr  7814  ltsopr  7815  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemdisj  7825  ltexprlemfl  7828  ltexprlemfu  7830  mulcmpblnrlemg  7959  cnegexlem2  8354  muladd  8562  eqord1  8662  eqord2  8663  divadddivap  8906  ltmul12a  9039  lemul12b  9040  cju  9140  zextlt  9571  supinfneg  9828  infsupneg  9829  xrre  10054  ixxdisj  10137  iooshf  10186  icodisj  10226  iccshftr  10228  iccshftl  10230  iccdil  10232  icccntr  10234  iccf1o  10238  fzaddel  10293  fzsubel  10294  seq3caopr  10756  seqcaoprg  10757  expineg2  10809  expsubap  10848  expnbnd  10924  facndiv  11000  hashfacen  11099  ccatpfx  11281  swrdccatfn  11304  swrdccatin2  11309  fprodeq0  12177  lcmdvds  12650  hashdvds  12792  eulerthlemh  12802  pceu  12867  pcqcl  12878  infpnlem1  12931  4sqlem11  12973  mhmpropd  13548  subsubm  13565  grplcan  13644  grplmulf1o  13656  dfgrp3mlem  13680  mulgfng  13710  mulgsubcl  13722  subsubg  13783  eqger  13810  resghm  13846  conjghm  13862  subsubrng  14227  subsubrg  14258  psrgrp  14698  txlm  15002  blininf  15147  xmeter  15159  xmetresbl  15163  limcimo  15388  dvdsppwf1o  15712  fsumdvdsmul  15714  sgmmul  15719  clwwlkn1loopb  16270