Theorem 3adant3r3 1268

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant3r3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3adant3r3

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1258	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1215	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  ressress  15765  plttr  16793  plelttr  16795  latledi  16912  latmlej11  16913  latmlej21  16915  latmlej22  16916  latjass  16918  latj12  16919  latj31  16922  ipopos  16983  latdisdlem  17012  imasmnd2  17150  imasmnd  17151  grpaddsubass  17328  grpsubsub4  17331  grpnpncan  17333  imasgrp2  17353  imasgrp  17354  frgp0  17996  cmn12  18036  abladdsub  18043  imasring  18442  dvrass  18513  lss1  18760  islmhm2  18859  psrgrp  19219  psrlmod  19222  zntoslem  19724  ipdir  19803  t1sep  20984  mettri2  21956  xmetrtri  21970  xmetrtri2  21971  pi1grplem  22657  dchrabl  24779  motgrp  25238  xmstrkgc  25566  ax5seglem4  25612  grpomuldivass  26779  ablomuldiv  26790  ablodivdiv4  26792  nvmdi  26887  dipdi  27082  dipsubdir  27087  dipsubdi  27088  cgr3tr4  31329  cgr3rflx  31331  seglemin  31390  linerflx1  31426  elicc3  31481  rngosubdi  32914  rngosubdir  32915  igenval2  33035  dmncan1  33045  latmassOLD  33534  omlfh1N  33563  omlfh3N  33564  cvrnbtwn  33576  cvrnbtwn2  33580  cvrnbtwn4  33584  hlatj12  33675  cvrntr  33729  islpln2a  33852  3atnelvolN  33890  elpadd2at2  34111  paddasslem17  34140  paddass  34142  paddssw2  34148  pmapjlln1  34159  ltrn2ateq  34485  cdlemc3  34498  cdleme1b  34531  cdleme3b  34534  cdleme3c  34535  cdleme9b  34557  erngdvlem3  35296  erngdvlem3-rN  35304  dvalveclem  35332  mendlmod  36782  lincsumscmcl  42016