Theorem 3adant3r3 1203

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3r3

Step	Hyp	Ref	Expression
1		ad4ant3.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1138	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1190	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  infsupprpr  9476  ressress  17339  plttr  18428  plelttr  18430  latledi  18565  latmlej11  18566  latmlej21  18568  latmlej22  18569  latjass  18571  latj12  18572  latj31  18575  latdisdlem  18584  ipopos  18624  imasmnd2  18881  imasmnd  18882  grpaddsubass  19153  grpsubsub4  19156  grpnpncan  19158  imasgrp2  19178  imasgrp  19179  frgp0  19887  cmn12  19929  abladdsub  19939  imasrng  20312  imasring  20471  dvrass  20549  isdomn4  20877  lss1  21122  islmhm2  21222  unichnlidl  21425  rspprop  21433  zntoslem  21769  ipdir  21852  psrlmod  22174  t1sep  23595  mettri2  24567  xmetrtri  24581  xmetrtri2  24582  pi1grplem  25277  dchrabl  27490  motgrp  28885  xmstrkgc  29342  ax5seglem4  29389  grpomuldivass  31022  ablomuldiv  31033  ablodivdiv4  31035  nvmdi  31129  dipdi  31324  dipsubdir  31329  dipsubdi  31330  cgr3tr4  36632  cgr3rflx  36634  seglemin  36693  linerflx1  36729  elicc3  36936  rngosubdi  38695  rngosubdir  38696  igenval2  38816  dmncan1  38826  latmassOLD  40102  omlfh1N  40131  omlfh3N  40132  cvrnbtwn  40144  cvrnbtwn2  40148  cvrnbtwn4  40152  hlatj12  40244  cvrntr  40298  islpln2a  40421  3atnelvolN  40459  elpadd2at2  40680  paddasslem17  40709  paddass  40711  paddssw2  40717  pmapjlln1  40728  ltrn2ateq  41053  cdlemc3  41066  cdleme1b  41099  cdleme3b  41102  cdleme3c  41103  cdleme9b  41125  erngdvlem3  41863  erngdvlem3-rN  41871  dvalveclem  41898  mendlmod  44030  lincsumscmcl  49363