Theorem 3adant3r3 1185

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 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1172	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  infsupprpr  9401  ressress  17165  plttr  18254  plelttr  18256  latledi  18391  latmlej11  18392  latmlej21  18394  latmlej22  18395  latjass  18397  latj12  18398  latj31  18401  latdisdlem  18410  ipopos  18450  imasmnd2  18690  imasmnd  18691  grpaddsubass  18951  grpsubsub4  18954  grpnpncan  18956  imasgrp2  18976  imasgrp  18977  frgp0  19680  cmn12  19722  abladdsub  19732  imasrng  20103  imasring  20257  dvrass  20335  isdomn4  20640  lss1  20880  islmhm2  20981  zntoslem  21502  ipdir  21585  psrlmod  21906  t1sep  23305  mettri2  24276  xmetrtri  24290  xmetrtri2  24291  pi1grplem  24996  dchrabl  27212  motgrp  28541  xmstrkgc  28884  ax5seglem4  28931  grpomuldivass  30542  ablomuldiv  30553  ablodivdiv4  30555  nvmdi  30649  dipdi  30844  dipsubdir  30849  dipsubdi  30850  cgr3tr4  36168  cgr3rflx  36170  seglemin  36229  linerflx1  36265  elicc3  36433  rngosubdi  38058  rngosubdir  38059  igenval2  38179  dmncan1  38189  latmassOLD  39401  omlfh1N  39430  omlfh3N  39431  cvrnbtwn  39443  cvrnbtwn2  39447  cvrnbtwn4  39451  hlatj12  39543  cvrntr  39597  islpln2a  39720  3atnelvolN  39758  elpadd2at2  39979  paddasslem17  40008  paddass  40010  paddssw2  40016  pmapjlln1  40027  ltrn2ateq  40352  cdlemc3  40365  cdleme1b  40398  cdleme3b  40401  cdleme3c  40402  cdleme9b  40424  erngdvlem3  41162  erngdvlem3-rN  41170  dvalveclem  41197  mendlmod  43346  lincsumscmcl  48595