Theorem 3ad2ant1 802

Description: Deduction adding conjuncts to an antecedent.

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (φ → χ)

Assertion

Ref	Expression
3ad2ant1	⊢ ((φ ⋀ ψ ⋀ θ) → χ)

Proof of Theorem 3ad2ant1

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (φ → χ)
2	1	adantr 391	. 2 ⊢ ((φ ⋀ θ) → χ)
3	2	3adant2 800	1 ⊢ ((φ ⋀ ψ ⋀ θ) → χ)

Syntax hints:   → wi 3   ⋀ w3a 777

This theorem is referenced by:  sbciegft 1962  itlso 2869  reuuniss 2895  oneo 4218  fodomr 4489  alephval3 4914  ltasr 5221  cnegextlem1 5357  divdivmult 5797  ltmulgt11t 5848  lt2mul2divt 5874  lediv2t 5893  ledivp1 5908  ltdivp1 5909  suprleub 6061  supxrun 6087  gtndivt 6195  lbicc2t 6405  icoshftf1olem 6411  eluzp1p1t 6436  infmssuzle 6466  eluzfz1t 6488  seqzvalt 6541  seqzval2t 6554  seqzcl 6559  expwordit 6604  expword2it 6606  expubndt 6609  sqlecant 6642  bernneq2 6654  expnlbndt 6656  fsum1p 7019  fsumshft 7031  serz1p 7052  serzmulc1 7057  iserzgt0 7211  isummulc1 7212  ivthlem6 7286  ivthlem7 7287  sin02gt0 7479  tgtop11t 7633  tgsst 7635  elcls3 7708  neiint 7716  neips 7724  opnneissb 7725  opnssneib 7726  islp2 7744  iscnp2 7758  cnpco 7766  cnconst 7777  bl2in 7840  metcnpf 7880  metcnp 7884  metidcn 7897  metdnsconst 7898  cncfmet 7902  tgioolem 7911  caussi 7951  iscms2lem4 7989  grpdivval 8078  imsdval 8313  nvelbl 8321  nvcnpf 8324  nvcni 8325  nvcni2 8326  nvlmle 8329  ipval 8349  lno0 8413  nvcnpi3 8418  nvcnpi4 8419  nmoubi 8431  nmobndi 8434  isblo3i 8457  phpar2 8478  phpar 8479  spwval2 8649  pilem1 8666  sinq12gt0t 8703  sincosq1eq 8704  efif1lem1 8725  efif1lem2 8726  his52t 8949  bcs2t 9044  spansncol 9486  pjspansnt 9495  nmoplbt 9826  nmopubt 9827  unopt 9834  hmopt 9841  nmfnlbt 9843  nmfnleubt 9844  lnopmult 9886  nmcopexlem5 9950  nmcfnexlem5 9979  leopmult 10062  hstelt 10137  ghomid 10389  ghomf1olem 10391  truni1 10485  homeofval 10502  hmphsyma 10514  homcard 10525  hmeobc 10528  fipfil2 10550  neifil 10553  filintf 10554  fgsb 10555  cnfilca 10562  rcfpfillem6 10568  mslb1 10600  2wsms 10601  1cat 10663  cmpmorp 10683  icmpmon 10715  idfisf 10731

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 779

Copyright terms: Public domain