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  1166  3ad2antr3  1167  xordidc  1419  foco  5521  fvun1  5658  isocnv  5893  isores2  5895  f1oiso2  5909  offval  6179  xp2nd  6265  1stconst  6320  2ndconst  6321  tfrlem9  6418  nnmordi  6615  dom2lem  6876  fundmen  6912  mapen  6958  ssenen  6963  ltsonq  7531  ltexnqq  7541  genprndl  7654  genprndu  7655  ltpopr  7728  ltsopr  7729  ltexprlemm  7733  ltexprlemopl  7734  ltexprlemopu  7736  ltexprlemdisj  7739  ltexprlemfl  7742  ltexprlemfu  7744  mulcmpblnrlemg  7873  cnegexlem2  8268  muladd  8476  eqord1  8576  eqord2  8577  divadddivap  8820  ltmul12a  8953  lemul12b  8954  cju  9054  zextlt  9485  supinfneg  9736  infsupneg  9737  xrre  9962  ixxdisj  10045  iooshf  10094  icodisj  10134  iccshftr  10136  iccshftl  10138  iccdil  10140  icccntr  10142  iccf1o  10146  fzaddel  10201  fzsubel  10202  seq3caopr  10662  seqcaoprg  10663  expineg2  10715  expsubap  10754  expnbnd  10830  facndiv  10906  hashfacen  11003  ccatpfx  11177  fprodeq0  12003  lcmdvds  12476  hashdvds  12618  eulerthlemh  12628  pceu  12693  pcqcl  12704  infpnlem1  12757  4sqlem11  12799  mhmpropd  13373  subsubm  13390  grplcan  13469  grplmulf1o  13481  dfgrp3mlem  13505  mulgfng  13535  mulgsubcl  13547  subsubg  13608  eqger  13635  resghm  13671  conjghm  13687  subsubrng  14051  subsubrg  14082  psrgrp  14522  txlm  14826  blininf  14971  xmeter  14983  xmetresbl  14987  limcimo  15212  dvdsppwf1o  15536  fsumdvdsmul  15538  sgmmul  15543