ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3ad2ant1 GIF version

Theorem 3ad2ant1 960
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1 (𝜑𝜒)
Assertion
Ref Expression
3ad2ant1 ((𝜑𝜓𝜃) → 𝜒)

Proof of Theorem 3ad2ant1
StepHypRef Expression
1 3ad2ant.1 . . 3 (𝜑𝜒)
21adantr 270 . 2 ((𝜑𝜃) → 𝜒)
323adant2 958 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  simp1l  963  simp1r  964  simp11  969  simp12  970  simp13  971  simp1ll  1002  simp1lr  1003  simp1rl  1004  simp1rr  1005  simp1l1  1032  simp1l2  1033  simp1l3  1034  simp1r1  1035  simp1r2  1036  simp1r3  1037  simp11l  1050  simp11r  1051  simp12l  1052  simp12r  1053  simp13l  1054  simp13r  1055  simp111  1068  simp112  1069  simp113  1070  simp121  1071  simp122  1072  simp123  1073  simp131  1074  simp132  1075  simp133  1076  3anim123i  1124  3jaao  1240  ceqsalt  2626  sbciegft  2845  reupick2  3257  ifbothdc  3388  frirrg  4113  breldmg  4569  fntpg  4986  funimaexglem  5013  fex2  5090  fvun1  5271  fprg  5378  fsnunfv  5395  fnfvima  5425  cocan1  5458  cocan2  5459  mpt2fvex  5860  poxp  5884  smoiso  5951  tfrlem5  5963  tfrlemibxssdm  5976  tfr1onlembfn  5993  tfri1dALT  6000  tfrcllembfn  6006  rdgon  6035  freccllem  6051  nnawordex  6167  fidceq  6404  fidifsnen  6405  dif1en  6414  en2eqpr  6434  unsnfi  6439  unsnfidcex  6440  unsnfidcel  6441  ordiso2  6505  mulcanenq0ec  6697  prltlu  6739  prarloclem3step  6748  prarloclem5  6752  ltasrg  7009  cnegexlem1  7350  addcan  7355  apcotr  7774  apadd1  7775  mulext1  7779  divdivap1  7878  divdivap2  7879  div2negap  7890  divneg2ap  7891  ltmulgt11  8009  ltdiv2  8032  squeeze0  8049  nndivtr  8147  nn0n0n1ge2  8499  zdivmul  8518  gtndiv  8523  eluzuzle  8708  eluzp1p1  8725  qdivcl  8809  irrmul  8813  rpgecl  8843  lbico1  9029  lbicc2  9082  zltaddlt1le  9104  uzsubsubfz  9142  elfz1b  9183  elfz0ubfz0  9213  fz0fzelfz0  9215  difelfzle  9222  difelfznle  9223  2ffzeq  9228  fzo1fzo0n0  9269  ubmelfzo  9286  fzonn0p1p1  9299  elfzom1p1elfzo  9300  elfzonelfzo  9316  subfzo0  9328  ceiqle  9395  ceilqle  9396  modqval  9406  flqpmodeq  9409  modq0  9411  negqmod0  9413  modqge0  9414  modqlt  9415  modqdiffl  9417  modqmulnn  9424  modqvalp1  9425  modqmuladdnn0  9450  qnegmod  9451  addmodid  9454  modfzo0difsn  9477  addmodlteq  9480  qexpclz  9594  expgt1  9611  expp1zap  9622  expm1ap  9623  expubnd  9630  bernneq2  9691  expnlbnd  9694  omgadd  9826  sizeun  9829  shftuz  9843  mulreap  9889  redivap  9899  imdivap  9906  resqrtcl  10053  climuni  10270  addcn2  10287  mulcn2  10289  dvdsval2  10343  addmodlteqALT  10404  modremain  10473  fldivndvdslt  10479  mulgcdr  10551  gcddiv  10552  rpmulgcd  10559  rplpwr  10560  rppwr  10561  qredeq  10622  divgcdcoprmex  10628  cncongr1  10629  cncongr2  10630  dvdsnprmd  10651  euclemma  10669  prmexpb  10674  unennn  10708  bdfind  10899
  Copyright terms: Public domain W3C validator