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  1165  3ad2antr3  1166  xordidc  1418  foco  5503  fvun1  5639  isocnv  5870  isores2  5872  f1oiso2  5886  offval  6156  xp2nd  6242  1stconst  6297  2ndconst  6298  tfrlem9  6395  nnmordi  6592  dom2lem  6849  fundmen  6883  mapen  6925  ssenen  6930  ltsonq  7493  ltexnqq  7503  genprndl  7616  genprndu  7617  ltpopr  7690  ltsopr  7691  ltexprlemm  7695  ltexprlemopl  7696  ltexprlemopu  7698  ltexprlemdisj  7701  ltexprlemfl  7704  ltexprlemfu  7706  mulcmpblnrlemg  7835  cnegexlem2  8230  muladd  8438  eqord1  8538  eqord2  8539  divadddivap  8782  ltmul12a  8915  lemul12b  8916  cju  9016  zextlt  9447  supinfneg  9698  infsupneg  9699  xrre  9924  ixxdisj  10007  iooshf  10056  icodisj  10096  iccshftr  10098  iccshftl  10100  iccdil  10102  icccntr  10104  iccf1o  10108  fzaddel  10163  fzsubel  10164  seq3caopr  10621  seqcaoprg  10622  expineg2  10674  expsubap  10713  expnbnd  10789  facndiv  10865  hashfacen  10962  fprodeq0  11847  lcmdvds  12320  hashdvds  12462  eulerthlemh  12472  pceu  12537  pcqcl  12548  infpnlem1  12601  4sqlem11  12643  mhmpropd  13216  subsubm  13233  grplcan  13312  grplmulf1o  13324  dfgrp3mlem  13348  mulgfng  13378  mulgsubcl  13390  subsubg  13451  eqger  13478  resghm  13514  conjghm  13530  subsubrng  13894  subsubrg  13925  psrgrp  14365  txlm  14669  blininf  14814  xmeter  14826  xmetresbl  14830  limcimo  15055  dvdsppwf1o  15379  fsumdvdsmul  15381  sgmmul  15386