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  5494  fvun1  5630  isocnv  5861  isores2  5863  f1oiso2  5877  offval  6147  xp2nd  6233  1stconst  6288  2ndconst  6289  tfrlem9  6386  nnmordi  6583  dom2lem  6840  fundmen  6874  mapen  6916  ssenen  6921  ltsonq  7484  ltexnqq  7494  genprndl  7607  genprndu  7608  ltpopr  7681  ltsopr  7682  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemdisj  7692  ltexprlemfl  7695  ltexprlemfu  7697  mulcmpblnrlemg  7826  cnegexlem2  8221  muladd  8429  eqord1  8529  eqord2  8530  divadddivap  8773  ltmul12a  8906  lemul12b  8907  cju  9007  zextlt  9437  supinfneg  9688  infsupneg  9689  xrre  9914  ixxdisj  9997  iooshf  10046  icodisj  10086  iccshftr  10088  iccshftl  10090  iccdil  10092  icccntr  10094  iccf1o  10098  fzaddel  10153  fzsubel  10154  seq3caopr  10606  seqcaoprg  10607  expineg2  10659  expsubap  10698  expnbnd  10774  facndiv  10850  hashfacen  10947  fprodeq0  11801  lcmdvds  12274  hashdvds  12416  eulerthlemh  12426  pceu  12491  pcqcl  12502  infpnlem1  12555  4sqlem11  12597  mhmpropd  13170  subsubm  13187  grplcan  13266  grplmulf1o  13278  dfgrp3mlem  13302  mulgfng  13332  mulgsubcl  13344  subsubg  13405  eqger  13432  resghm  13468  conjghm  13484  subsubrng  13848  subsubrg  13879  psrgrp  14319  txlm  14623  blininf  14768  xmeter  14780  xmetresbl  14784  limcimo  15009  dvdsppwf1o  15333  fsumdvdsmul  15335  sgmmul  15340