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  5508  fvun1  5644  isocnv  5879  isores2  5881  f1oiso2  5895  offval  6165  xp2nd  6251  1stconst  6306  2ndconst  6307  tfrlem9  6404  nnmordi  6601  dom2lem  6862  fundmen  6897  mapen  6942  ssenen  6947  ltsonq  7510  ltexnqq  7520  genprndl  7633  genprndu  7634  ltpopr  7707  ltsopr  7708  ltexprlemm  7712  ltexprlemopl  7713  ltexprlemopu  7715  ltexprlemdisj  7718  ltexprlemfl  7721  ltexprlemfu  7723  mulcmpblnrlemg  7852  cnegexlem2  8247  muladd  8455  eqord1  8555  eqord2  8556  divadddivap  8799  ltmul12a  8932  lemul12b  8933  cju  9033  zextlt  9464  supinfneg  9715  infsupneg  9716  xrre  9941  ixxdisj  10024  iooshf  10073  icodisj  10113  iccshftr  10115  iccshftl  10117  iccdil  10119  icccntr  10121  iccf1o  10125  fzaddel  10180  fzsubel  10181  seq3caopr  10638  seqcaoprg  10639  expineg2  10691  expsubap  10730  expnbnd  10806  facndiv  10882  hashfacen  10979  fprodeq0  11870  lcmdvds  12343  hashdvds  12485  eulerthlemh  12495  pceu  12560  pcqcl  12571  infpnlem1  12624  4sqlem11  12666  mhmpropd  13240  subsubm  13257  grplcan  13336  grplmulf1o  13348  dfgrp3mlem  13372  mulgfng  13402  mulgsubcl  13414  subsubg  13475  eqger  13502  resghm  13538  conjghm  13554  subsubrng  13918  subsubrg  13949  psrgrp  14389  txlm  14693  blininf  14838  xmeter  14850  xmetresbl  14854  limcimo  15079  dvdsppwf1o  15403  fsumdvdsmul  15405  sgmmul  15410