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  4340  sotricim  4354  fmptco  5724  fvtp1g  5766  dff13  5811  fcof1o  5832  isocnv  5854  isores2  5856  isoini  5861  f1oiso2  5870  acexmidlemab  5912  ovmpodf  6050  offval  6138  xp1st  6218  1stconst  6274  cnvf1olem  6277  f1od2  6288  mpoxopoveq  6293  nnaordi  6561  nnmordi  6569  erinxp  6663  dom2lem  6826  fundmen  6860  pw2f1odclem  6890  mapen  6902  ssenen  6907  fidifsnen  6926  difinfsnlem  7158  fodjum  7205  cc2lem  7326  ltsonq  7458  lt2addnq  7464  lt2mulnq  7465  ltexnqq  7468  prarloclemarch2  7479  enq0sym  7492  genprndl  7581  genprndu  7582  prmuloc  7626  distrlem1prl  7642  distrlem1pru  7643  ltsopr  7656  ltexprlemdisj  7666  ltexprlemfl  7669  ltexprlemfu  7671  addcanprlemu  7675  ltaprg  7679  mulcmpblnrlemg  7800  recexgt0sr  7833  mul4  8151  2addsub  8233  muladd  8403  ltleadd  8465  eqord1  8502  eqord2  8503  divmulap3  8696  divcanap7  8740  divadddivap  8746  lemul2a  8878  lemul12b  8880  ltmuldiv2  8894  ltdivmul  8895  ltdivmul2  8897  ledivmul2  8899  lemuldiv2  8901  lt2msq  8905  cju  8980  zextlt  9409  xrlttr  9861  xrre3  9888  ixxdisj  9969  iooshf  10018  icodisj  10058  iccf1o  10070  seqf1og  10592  expsubap  10658  bcval5  10834  hashfacen  10907  seq3coll  10913  sqrt0rlem  11147  lenegsq  11239  zsumdc  11527  fisum0diag2  11590  prodmodclem2  11720  zproddc  11722  ndvdsadd  12072  zssinfcl  12085  lcmdvds  12217  oddpwdclemdc  12311  hashdvds  12359  phisum  12378  pcqmul  12441  pcmpt  12481  4sqlemffi  12534  4sqlem11  12539  ennnfonelemex  12571  grpinvid1  13124  grpinvid2  13125  grplcan  13134  grpnpncan0  13168  dfgrp3mlem  13170  dfgrp3m  13171  grplactcnv  13174  0nsg  13284  eqger  13294  resghm  13330  conjghm  13346  znunit  14147  eltg2  14221  ssnei2  14325  restopnb  14349  txdis1cn  14446  txlm  14447  elbl2ps  14560  elbl2  14561  blininf  14592  xmeter  14604  xmetresbl  14608  bdxmet  14669  metrest  14674  dedekindicc  14787  limcimo  14819  lgsquadlem1  15191