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  962  3ad2antr1  1164  xordidc  1410  po2nr  4345  sotricim  4359  fmptco  5731  fvtp1g  5773  dff13  5818  fcof1o  5839  isocnv  5861  isores2  5863  isoini  5868  f1oiso2  5877  acexmidlemab  5919  ovmpodf  6058  offval  6147  xp1st  6232  1stconst  6288  cnvf1olem  6291  f1od2  6302  mpoxopoveq  6307  nnaordi  6575  nnmordi  6583  erinxp  6677  dom2lem  6840  fundmen  6874  pw2f1odclem  6904  mapen  6916  ssenen  6921  fidifsnen  6940  difinfsnlem  7174  fodjum  7221  cc2lem  7351  ltsonq  7484  lt2addnq  7490  lt2mulnq  7491  ltexnqq  7494  prarloclemarch2  7505  enq0sym  7518  genprndl  7607  genprndu  7608  prmuloc  7652  distrlem1prl  7668  distrlem1pru  7669  ltsopr  7682  ltexprlemdisj  7692  ltexprlemfl  7695  ltexprlemfu  7697  addcanprlemu  7701  ltaprg  7705  mulcmpblnrlemg  7826  recexgt0sr  7859  mul4  8177  2addsub  8259  muladd  8429  ltleadd  8492  eqord1  8529  eqord2  8530  divmulap3  8723  divcanap7  8767  divadddivap  8773  lemul2a  8905  lemul12b  8907  ltmuldiv2  8921  ltdivmul  8922  ltdivmul2  8924  ledivmul2  8926  lemuldiv2  8928  lt2msq  8932  cju  9007  zextlt  9437  xrlttr  9889  xrre3  9916  ixxdisj  9997  iooshf  10046  icodisj  10086  iccf1o  10098  zssinfcl  10341  seqf1og  10632  expsubap  10698  bcval5  10874  hashfacen  10947  seq3coll  10953  sqrt0rlem  11187  lenegsq  11279  zsumdc  11568  fisum0diag2  11631  prodmodclem2  11761  zproddc  11763  ndvdsadd  12115  lcmdvds  12274  oddpwdclemdc  12368  hashdvds  12416  phisum  12436  pcqmul  12499  pcmpt  12539  4sqlemffi  12592  4sqlem11  12597  ennnfonelemex  12658  grpinvid1  13256  grpinvid2  13257  grplcan  13266  grpnpncan0  13300  dfgrp3mlem  13302  dfgrp3m  13303  grplactcnv  13306  0nsg  13422  eqger  13432  resghm  13468  conjghm  13484  znunit  14293  psrgrp  14315  eltg2  14375  ssnei2  14479  restopnb  14503  txdis1cn  14600  txlm  14601  elbl2ps  14714  elbl2  14715  blininf  14746  xmeter  14758  xmetresbl  14762  bdxmet  14823  metrest  14828  dedekindicc  14955  limcimo  14987  dvmptfsum  15047  plycolemc  15080  dvdsppwf1o  15311  fsumdvdsmul  15313  sgmmul  15318  lgsquadlem1  15404  lgsquadlem2  15405  lgsquad2lem2  15409