Theorem adantrl 482

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 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad2ant2l  512  ad2ant2rl  515  3ad2antr2  1194  3ad2antr3  1195  xordidc  1448  opabssxpd  4811  foco  5626  fvun1  5769  isocnv  6017  isores2  6019  f1oiso2  6033  offval  6310  xp2nd  6400  1stconst  6457  2ndconst  6458  tfrlem9  6590  nnmordi  6789  dom2lem  7058  fundmen  7094  mapen  7146  mapunen  7151  ssenen  7152  ltsonq  7766  ltexnqq  7776  genprndl  7889  genprndu  7890  ltpopr  7963  ltsopr  7964  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemdisj  7974  ltexprlemfl  7977  ltexprlemfu  7979  mulcmpblnrlemg  8108  cnegexlem2  8504  muladd  8713  eqord1  8813  eqord2  8814  divadddivap  9060  ltmul12a  9193  lemul12b  9194  cju  9294  zextlt  9743  supinfneg  10005  infsupneg  10006  xrre  10233  ixxdisj  10316  iooshf  10365  icodisj  10405  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  iccf1o  10418  fzaddel  10476  fzsubel  10477  seq3caopr  10947  seqcaoprg  10948  expineg2  11000  expsubap  11039  expnbnd  11116  facndiv  11193  hashfibclem  11298  hashfacen  11300  hashf1lem1  11301  ccatpfx  11489  swrdccatfn  11512  swrdccatin2  11517  fprodeq0  12403  lcmdvds  12876  hashdvds  13022  eulerthlemh  13032  pceu  13097  pcqcl  13108  infpnlem1  13161  4sqlem11  13203  mhmpropd  13826  subsubm  13843  grplcan  13920  grplmulf1o  13932  dfgrp3mlem  13956  mulgfng  13980  mulgsubcl  13992  subsubg  14053  eqger  14080  resghm  14116  conjghm  14132  subsubrng  14606  subsubrg  14637  issubassa2  15119  psrbagconf1o  15149  psrgrp  15167  txlm  15471  blininf  15616  xmeter  15628  xmetresbl  15632  limcimo  15857  dvdsppwf1o  16244  fsumdvdsmul  16246  sgmmul  16251  bposlem6  16277  clwwlkn1loopb  16827