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  1410  foco  5488  fvun1  5624  isocnv  5855  isores2  5857  f1oiso2  5871  offval  6140  xp2nd  6221  1stconst  6276  2ndconst  6277  tfrlem9  6374  nnmordi  6571  dom2lem  6828  fundmen  6862  mapen  6904  ssenen  6909  ltsonq  7460  ltexnqq  7470  genprndl  7583  genprndu  7584  ltpopr  7657  ltsopr  7658  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemdisj  7668  ltexprlemfl  7671  ltexprlemfu  7673  mulcmpblnrlemg  7802  cnegexlem2  8197  muladd  8405  eqord1  8504  eqord2  8505  divadddivap  8748  ltmul12a  8881  lemul12b  8882  cju  8982  zextlt  9412  supinfneg  9663  infsupneg  9664  xrre  9889  ixxdisj  9972  iooshf  10021  icodisj  10061  iccshftr  10063  iccshftl  10065  iccdil  10067  icccntr  10069  iccf1o  10073  fzaddel  10128  fzsubel  10129  seq3caopr  10569  seqcaoprg  10570  expineg2  10622  expsubap  10661  expnbnd  10737  facndiv  10813  hashfacen  10910  fprodeq0  11763  lcmdvds  12220  hashdvds  12362  eulerthlemh  12372  pceu  12436  pcqcl  12447  infpnlem1  12500  4sqlem11  12542  mhmpropd  13041  subsubm  13058  grplcan  13137  grplmulf1o  13149  dfgrp3mlem  13173  mulgfng  13197  mulgsubcl  13209  subsubg  13270  eqger  13297  resghm  13333  conjghm  13349  subsubrng  13713  subsubrg  13744  txlm  14458  blininf  14603  xmeter  14615  xmetresbl  14619  limcimo  14844