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

Theorem 3ad2ant1 1002
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 274 . 2 ((𝜑𝜃) → 𝜒)
323adant2 1000 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  simp1l  1005  simp1r  1006  simp11  1011  simp12  1012  simp13  1013  simp1ll  1044  simp1lr  1045  simp1rl  1046  simp1rr  1047  simp1l1  1074  simp1l2  1075  simp1l3  1076  simp1r1  1077  simp1r2  1078  simp1r3  1079  simp11l  1092  simp11r  1093  simp12l  1094  simp12r  1095  simp13l  1096  simp13r  1097  simp111  1110  simp112  1111  simp113  1112  simp121  1113  simp122  1114  simp123  1115  simp131  1116  simp132  1117  simp133  1118  3anim123i  1166  3jaao  1286  ceqsalt  2712  sbciegft  2939  reupick2  3362  ifbothdc  3504  frirrg  4272  breldmg  4745  fntpg  5179  funimaexglem  5206  fex2  5291  fvun1  5487  fprg  5603  fsnunfv  5621  fnfvima  5652  cocan1  5688  cocan2  5689  mpoeq3dv  5837  mpofvex  6101  poxp  6129  smoiso  6199  tfrlem5  6211  tfrlemibxssdm  6224  tfr1onlembfn  6241  tfri1dALT  6248  tfrcllembfn  6254  rdgon  6283  freccllem  6299  nnawordex  6424  mapxpen  6742  fidceq  6763  fidifsnen  6764  dif1en  6773  en2eqpr  6801  unsnfi  6807  unsnfidcex  6808  unsnfidcel  6809  fisseneq  6820  ordiso2  6920  updjud  6967  mkvprop  7032  endjudisj  7066  xpdjuen  7074  mulcanenq0ec  7253  prltlu  7295  prarloclem3step  7304  prarloclem5  7308  ltasrg  7578  cnegexlem1  7937  addcan  7942  apcotr  8369  apadd1  8370  mulext1  8374  divdivap1  8483  divdivap2  8484  div2negap  8495  divneg2ap  8496  ltmulgt11  8622  ltdiv2  8645  squeeze0  8662  nndivtr  8762  nn0n0n1ge2  9121  zdivmul  9141  gtndiv  9146  eluzuzle  9334  eluzp1p1  9351  qdivcl  9435  irrmul  9439  rpgecl  9470  xaddass  9652  xltadd1  9659  xlt2add  9663  lbico1  9713  lbicc2  9767  zltaddlt1le  9789  uzsubsubfz  9827  elfz1b  9870  elfz0ubfz0  9902  fz0fzelfz0  9904  difelfzle  9911  difelfznle  9912  2ffzeq  9918  fzo1fzo0n0  9960  ubmelfzo  9977  fzonn0p1p1  9990  elfzom1p1elfzo  9991  elfzonelfzo  10007  subfzo0  10019  ceiqle  10086  ceilqle  10087  modqval  10097  flqpmodeq  10100  modq0  10102  negqmod0  10104  modqge0  10105  modqlt  10106  modqdiffl  10108  modqmulnn  10115  modqvalp1  10116  modqmuladdnn0  10141  qnegmod  10142  addmodid  10145  modfzo0difsn  10168  addmodlteq  10171  qexpclz  10314  expgt1  10331  expp1zap  10342  expm1ap  10343  expubnd  10350  bernneq2  10413  expnlbnd  10416  omgadd  10548  hashun  10551  fihashssdif  10564  hashdifpr  10566  fimaxq  10573  shftuz  10589  mulreap  10636  redivap  10646  imdivap  10653  resqrtcl  10801  xrmaxltsup  11027  xrmaxaddlem  11029  xrmaxadd  11030  xrlemininf  11040  xrminltinf  11041  climuni  11062  addcn2  11079  mulcn2  11081  efsub  11387  sin02gt0  11470  cos12dec  11474  dvdsval2  11496  addmodlteqALT  11557  modremain  11626  fldivndvdslt  11632  mulgcdr  11706  gcddiv  11707  rpmulgcd  11714  rplpwr  11715  rppwr  11716  qredeq  11777  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  dvdsnprmd  11806  euclemma  11824  prmexpb  11829  qnumdenbi  11870  hashgcdlem  11903  unennn  11910  setsex  11991  basgen  12249  2basgeng  12251  iuncld  12284  neipsm  12323  opnneissb  12324  opnssneib  12325  iscnp3  12372  cnprcl2k  12375  cnpnei  12388  cncnp2m  12400  cnptoprest  12408  sslm  12416  upxp  12441  cnmpt22  12463  distspace  12504  0met  12553  blvalps  12557  blval  12558  ssblps  12594  ssbl  12595  blpnfctr  12608  blopn  12659  blnei  12661  bdxmet  12670  bdbl  12672  metcnp3  12680  tgqioo  12716  ptolemy  12905  sinq12gt0  12911  sincosq1eq  12920  bdfind  13144
  Copyright terms: Public domain W3C validator