Theorem adantrr 479

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

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		simpl 109	. 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:  ad2ant2r  509  ad2ant2lr  510  dn1dc  969  3ad2antr1  1189  xordidc  1444  po2nr  4429  sotricim  4443  fmptco  5842  fvtp1g  5891  dff13  5940  fcof1o  5961  isocnv  5983  isores2  5985  isoini  5990  f1oiso2  5999  acexmidlemab  6043  ovmpodf  6184  offval  6273  xp1st  6358  1stconst  6416  cnvf1olem  6419  f1od2  6430  mpoxopoveq  6470  nnaordi  6740  nnmordi  6748  erinxp  6842  dom2lem  7010  fundmen  7046  pw2f1odclem  7086  mapen  7098  ssenen  7104  fidifsnen  7124  difinfsnlem  7389  fodjum  7436  cc2lem  7576  ltsonq  7709  lt2addnq  7715  lt2mulnq  7716  ltexnqq  7719  prarloclemarch2  7730  enq0sym  7743  genprndl  7832  genprndu  7833  prmuloc  7877  distrlem1prl  7893  distrlem1pru  7894  ltsopr  7907  ltexprlemdisj  7917  ltexprlemfl  7920  ltexprlemfu  7922  addcanprlemu  7926  ltaprg  7930  mulcmpblnrlemg  8051  recexgt0sr  8084  mul4  8401  2addsub  8483  muladd  8653  ltleadd  8716  eqord1  8753  eqord2  8754  divmulap3  8947  divcanap7  8991  divadddivap  8997  lemul2a  9129  lemul12b  9131  ltmuldiv2  9145  ltdivmul  9146  ltdivmul2  9148  ledivmul2  9150  lemuldiv2  9152  lt2msq  9156  cju  9231  zextlt  9666  xrlttr  10124  xrre3  10151  ixxdisj  10232  iooshf  10281  icodisj  10321  iccf1o  10334  zssinfcl  10588  seqf1og  10879  expsubap  10945  bcval5  11121  hashfacen  11201  seq3coll  11207  swrdswrdlem  11389  swrdccatin2  11414  sqrt0rlem  11681  lenegsq  11773  zsumdc  12063  fisum0diag2  12126  prodmodclem2  12256  zproddc  12258  ndvdsadd  12610  lcmdvds  12769  oddpwdclemdc  12863  hashdvds  12911  phisum  12931  pcqmul  12994  pcmpt  13034  4sqlemffi  13087  4sqlem11  13092  ennnfonelemex  13154  grpinvid1  13754  grpinvid2  13755  grplcan  13764  grpnpncan0  13798  dfgrp3mlem  13800  dfgrp3m  13801  grplactcnv  13804  0nsg  13920  eqger  13930  resghm  13966  conjghm  13982  znunit  14794  psrbagconf1o  14815  psrgrp  14827  eltg2  14905  ssnei2  15009  restopnb  15033  txdis1cn  15130  txlm  15131  elbl2ps  15244  elbl2  15245  blininf  15276  xmeter  15288  xmetresbl  15292  bdxmet  15353  metrest  15358  dedekindicc  15485  limcimo  15517  dvmptfsum  15577  plycolemc  15610  dvdsppwf1o  15844  fsumdvdsmul  15846  sgmmul  15851  lgsquadlem1  15937  lgsquadlem2  15938  lgsquad2lem2  15942  upgriswlkdc  16342