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  4786  foco  5601  fvun1  5743  isocnv  5984  isores2  5986  f1oiso2  6000  offval  6274  xp2nd  6360  1stconst  6417  2ndconst  6418  tfrlem9  6550  nnmordi  6749  dom2lem  7011  fundmen  7047  mapen  7099  mapunen  7104  ssenen  7105  ltsonq  7713  ltexnqq  7723  genprndl  7836  genprndu  7837  ltpopr  7910  ltsopr  7911  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemopu  7918  ltexprlemdisj  7921  ltexprlemfl  7924  ltexprlemfu  7926  mulcmpblnrlemg  8055  cnegexlem2  8449  muladd  8657  eqord1  8757  eqord2  8758  divadddivap  9001  ltmul12a  9134  lemul12b  9135  cju  9235  zextlt  9670  supinfneg  9927  infsupneg  9928  xrre  10153  ixxdisj  10236  iooshf  10285  icodisj  10325  iccshftr  10327  iccshftl  10329  iccdil  10331  icccntr  10333  iccf1o  10338  fzaddel  10393  fzsubel  10394  seq3caopr  10857  seqcaoprg  10858  expineg2  10910  expsubap  10949  expnbnd  11025  facndiv  11101  hashfibclem  11206  hashfacen  11208  ccatpfx  11393  swrdccatfn  11416  swrdccatin2  11421  fprodeq0  12303  lcmdvds  12776  hashdvds  12918  eulerthlemh  12928  pceu  12993  pcqcl  13004  infpnlem1  13057  4sqlem11  13099  mhmpropd  13679  subsubm  13696  grplcan  13775  grplmulf1o  13787  dfgrp3mlem  13811  mulgfng  13841  mulgsubcl  13853  subsubg  13914  eqger  13941  resghm  13977  conjghm  13993  subsubrng  14359  subsubrg  14390  psrbagconf1o  14828  psrgrp  14840  txlm  15144  blininf  15289  xmeter  15301  xmetresbl  15305  limcimo  15530  dvdsppwf1o  15857  fsumdvdsmul  15859  sgmmul  15864  clwwlkn1loopb  16415