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  opabssxpd  4760  foco  5567  fvun1  5708  isocnv  5947  isores2  5949  f1oiso2  5963  offval  6238  xp2nd  6324  1stconst  6381  2ndconst  6382  tfrlem9  6480  nnmordi  6679  dom2lem  6940  fundmen  6976  mapen  7027  ssenen  7032  ltsonq  7608  ltexnqq  7618  genprndl  7731  genprndu  7732  ltpopr  7805  ltsopr  7806  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemdisj  7816  ltexprlemfl  7819  ltexprlemfu  7821  mulcmpblnrlemg  7950  cnegexlem2  8345  muladd  8553  eqord1  8653  eqord2  8654  divadddivap  8897  ltmul12a  9030  lemul12b  9031  cju  9131  zextlt  9562  supinfneg  9819  infsupneg  9820  xrre  10045  ixxdisj  10128  iooshf  10177  icodisj  10217  iccshftr  10219  iccshftl  10221  iccdil  10223  icccntr  10225  iccf1o  10229  fzaddel  10284  fzsubel  10285  seq3caopr  10747  seqcaoprg  10748  expineg2  10800  expsubap  10839  expnbnd  10915  facndiv  10991  hashfacen  11090  ccatpfx  11272  swrdccatfn  11295  swrdccatin2  11300  fprodeq0  12168  lcmdvds  12641  hashdvds  12783  eulerthlemh  12793  pceu  12858  pcqcl  12869  infpnlem1  12922  4sqlem11  12964  mhmpropd  13539  subsubm  13556  grplcan  13635  grplmulf1o  13647  dfgrp3mlem  13671  mulgfng  13701  mulgsubcl  13713  subsubg  13774  eqger  13801  resghm  13837  conjghm  13853  subsubrng  14218  subsubrg  14249  psrgrp  14689  txlm  14993  blininf  15138  xmeter  15150  xmetresbl  15154  limcimo  15379  dvdsppwf1o  15703  fsumdvdsmul  15705  sgmmul  15710  clwwlkn1loopb  16215