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

Theorem 3ad2ant1 987
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 985 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 947
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 949
This theorem is referenced by:  simp1l  990  simp1r  991  simp11  996  simp12  997  simp13  998  simp1ll  1029  simp1lr  1030  simp1rl  1031  simp1rr  1032  simp1l1  1059  simp1l2  1060  simp1l3  1061  simp1r1  1062  simp1r2  1063  simp1r3  1064  simp11l  1077  simp11r  1078  simp12l  1079  simp12r  1080  simp13l  1081  simp13r  1082  simp111  1095  simp112  1096  simp113  1097  simp121  1098  simp122  1099  simp123  1100  simp131  1101  simp132  1102  simp133  1103  3anim123i  1151  3jaao  1271  ceqsalt  2686  sbciegft  2911  reupick2  3332  ifbothdc  3474  frirrg  4242  breldmg  4715  fntpg  5149  funimaexglem  5176  fex2  5261  fvun1  5455  fprg  5571  fsnunfv  5589  fnfvima  5620  cocan1  5656  cocan2  5657  mpoeq3dv  5805  mpofvex  6069  poxp  6097  smoiso  6167  tfrlem5  6179  tfrlemibxssdm  6192  tfr1onlembfn  6209  tfri1dALT  6216  tfrcllembfn  6222  rdgon  6251  freccllem  6267  nnawordex  6392  mapxpen  6710  fidceq  6731  fidifsnen  6732  dif1en  6741  en2eqpr  6769  unsnfi  6775  unsnfidcex  6776  unsnfidcel  6777  fisseneq  6788  ordiso2  6888  updjud  6935  mkvprop  7000  endjudisj  7034  xpdjuen  7042  mulcanenq0ec  7221  prltlu  7263  prarloclem3step  7272  prarloclem5  7276  ltasrg  7546  cnegexlem1  7905  addcan  7910  apcotr  8336  apadd1  8337  mulext1  8341  divdivap1  8450  divdivap2  8451  div2negap  8462  divneg2ap  8463  ltmulgt11  8586  ltdiv2  8609  squeeze0  8626  nndivtr  8726  nn0n0n1ge2  9079  zdivmul  9099  gtndiv  9104  eluzuzle  9290  eluzp1p1  9307  qdivcl  9391  irrmul  9395  rpgecl  9425  xaddass  9607  xltadd1  9614  xlt2add  9618  lbico1  9668  lbicc2  9722  zltaddlt1le  9744  uzsubsubfz  9782  elfz1b  9825  elfz0ubfz0  9857  fz0fzelfz0  9859  difelfzle  9866  difelfznle  9867  2ffzeq  9873  fzo1fzo0n0  9915  ubmelfzo  9932  fzonn0p1p1  9945  elfzom1p1elfzo  9946  elfzonelfzo  9962  subfzo0  9974  ceiqle  10041  ceilqle  10042  modqval  10052  flqpmodeq  10055  modq0  10057  negqmod0  10059  modqge0  10060  modqlt  10061  modqdiffl  10063  modqmulnn  10070  modqvalp1  10071  modqmuladdnn0  10096  qnegmod  10097  addmodid  10100  modfzo0difsn  10123  addmodlteq  10126  qexpclz  10269  expgt1  10286  expp1zap  10297  expm1ap  10298  expubnd  10305  bernneq2  10368  expnlbnd  10371  omgadd  10503  hashun  10506  fihashssdif  10519  hashdifpr  10521  fimaxq  10528  shftuz  10544  mulreap  10591  redivap  10601  imdivap  10608  resqrtcl  10756  xrmaxltsup  10982  xrmaxaddlem  10984  xrmaxadd  10985  xrlemininf  10995  xrminltinf  10996  climuni  11017  addcn2  11034  mulcn2  11036  efsub  11301  sin02gt0  11384  cos12dec  11388  dvdsval2  11408  addmodlteqALT  11469  modremain  11538  fldivndvdslt  11544  mulgcdr  11618  gcddiv  11619  rpmulgcd  11626  rplpwr  11627  rppwr  11628  qredeq  11689  divgcdcoprmex  11695  cncongr1  11696  cncongr2  11697  dvdsnprmd  11718  euclemma  11736  prmexpb  11741  qnumdenbi  11781  hashgcdlem  11814  unennn  11821  setsex  11902  basgen  12160  2basgeng  12162  iuncld  12195  neipsm  12234  opnneissb  12235  opnssneib  12236  iscnp3  12283  cnprcl2k  12286  cnpnei  12299  cncnp2m  12311  cnptoprest  12319  sslm  12327  upxp  12352  cnmpt22  12374  distspace  12415  0met  12464  blvalps  12468  blval  12469  ssblps  12505  ssbl  12506  blpnfctr  12519  blopn  12570  blnei  12572  bdxmet  12581  bdbl  12583  metcnp3  12591  tgqioo  12627  ptolemy  12816  sinq12gt0  12822  bdfind  13040
  Copyright terms: Public domain W3C validator