Theorem 3adant3r3 1191

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  infsupprpr  9409  ressress  17208  plttr  18297  plelttr  18299  latledi  18434  latmlej11  18435  latmlej21  18437  latmlej22  18438  latjass  18440  latj12  18441  latj31  18444  latdisdlem  18453  ipopos  18493  imasmnd2  18733  imasmnd  18734  grpaddsubass  18997  grpsubsub4  19000  grpnpncan  19002  imasgrp2  19022  imasgrp  19023  frgp0  19726  cmn12  19768  abladdsub  19778  imasrng  20149  imasring  20301  dvrass  20379  isdomn4  20688  lss1  20928  islmhm2  21028  zntoslem  21531  ipdir  21614  psrlmod  21934  t1sep  23353  mettri2  24324  xmetrtri  24338  xmetrtri2  24339  pi1grplem  25034  dchrabl  27235  motgrp  28629  xmstrkgc  28972  ax5seglem4  29019  grpomuldivass  30630  ablomuldiv  30641  ablodivdiv4  30643  nvmdi  30737  dipdi  30932  dipsubdir  30937  dipsubdi  30938  cgr3tr4  36280  cgr3rflx  36282  seglemin  36341  linerflx1  36377  elicc3  36545  rngosubdi  38312  rngosubdir  38313  igenval2  38433  dmncan1  38443  latmassOLD  39721  omlfh1N  39750  omlfh3N  39751  cvrnbtwn  39763  cvrnbtwn2  39767  cvrnbtwn4  39771  hlatj12  39863  cvrntr  39917  islpln2a  40040  3atnelvolN  40078  elpadd2at2  40299  paddasslem17  40328  paddass  40330  paddssw2  40336  pmapjlln1  40347  ltrn2ateq  40672  cdlemc3  40685  cdleme1b  40718  cdleme3b  40721  cdleme3c  40722  cdleme9b  40744  erngdvlem3  41482  erngdvlem3-rN  41490  dvalveclem  41517  mendlmod  43634  lincsumscmcl  48924