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

Theorem 3ad2ant1 1018
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 276 . 2 ((𝜑𝜃) → 𝜒)
323adant2 1016 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  simp1l  1021  simp1r  1022  simp11  1027  simp12  1028  simp13  1029  simp1ll  1060  simp1lr  1061  simp1rl  1062  simp1rr  1063  simp1l1  1090  simp1l2  1091  simp1l3  1092  simp1r1  1093  simp1r2  1094  simp1r3  1095  simp11l  1108  simp11r  1109  simp12l  1110  simp12r  1111  simp13l  1112  simp13r  1113  simp111  1126  simp112  1127  simp113  1128  simp121  1129  simp122  1130  simp123  1131  simp131  1132  simp132  1133  simp133  1134  3anim123i  1184  3jaao  1308  ceqsalt  2763  sbciegft  2993  reupick2  3421  ifbothdc  3566  frirrg  4347  breldmg  4829  fntpg  5268  funimaexglem  5295  fex2  5380  fvun1  5578  fprg  5695  fsnunfv  5713  fnfvima  5746  cocan1  5782  cocan2  5783  mpoeq3dv  5935  funexw  6107  mpofvex  6198  poxp  6227  smoiso  6297  tfrlem5  6309  tfrlemibxssdm  6322  tfr1onlembfn  6339  tfri1dALT  6346  tfrcllembfn  6352  rdgon  6381  freccllem  6397  nnawordex  6524  mapxpen  6842  fidceq  6863  fidifsnen  6864  dif1en  6873  en2eqpr  6901  unsnfi  6912  unsnfidcex  6913  unsnfidcel  6914  fisseneq  6925  ordiso2  7028  updjud  7075  mkvprop  7150  endjudisj  7203  xpdjuen  7211  mulcanenq0ec  7432  prltlu  7474  prarloclem3step  7483  prarloclem5  7487  ltasrg  7757  cnegexlem1  8119  addcan  8124  apcotr  8551  apadd1  8552  mulext1  8556  divdivap1  8666  divdivap2  8667  div2negap  8678  divneg2ap  8679  ltmulgt11  8807  ltdiv2  8830  squeeze0  8847  nndivtr  8947  nn0n0n1ge2  9309  zdivmul  9329  gtndiv  9334  eluzuzle  9522  eluzp1p1  9539  qdivcl  9629  irrmul  9633  rpgecl  9666  xaddass  9853  xltadd1  9860  xlt2add  9864  lbico1  9914  lbicc2  9968  zltaddlt1le  9991  uzsubsubfz  10030  elfz1b  10073  elfz0ubfz0  10108  fz0fzelfz0  10110  difelfzle  10117  difelfznle  10118  2ffzeq  10124  fzo1fzo0n0  10166  ubmelfzo  10183  fzonn0p1p1  10196  elfzom1p1elfzo  10197  elfzonelfzo  10213  subfzo0  10225  ceiqle  10296  ceilqle  10297  modqval  10307  flqpmodeq  10310  modq0  10312  negqmod0  10314  modqge0  10315  modqlt  10316  modqdiffl  10318  modqmulnn  10325  modqvalp1  10326  modqmuladdnn0  10351  qnegmod  10352  addmodid  10355  modfzo0difsn  10378  addmodlteq  10381  qexpclz  10524  expgt1  10541  expp1zap  10552  expm1ap  10553  expubnd  10560  bernneq2  10624  expnlbnd  10627  omgadd  10763  hashun  10766  fihashssdif  10779  hashdifpr  10781  fimaxq  10788  shftuz  10807  mulreap  10854  redivap  10864  imdivap  10871  resqrtcl  11019  xrmaxltsup  11247  xrmaxaddlem  11249  xrmaxadd  11250  xrlemininf  11260  xrminltinf  11261  climuni  11282  addcn2  11299  mulcn2  11301  efsub  11670  sin02gt0  11752  cos12dec  11756  dvdsval2  11778  addmodlteqALT  11845  modremain  11914  fldivndvdslt  11920  mulgcdr  11999  gcddiv  12000  rpmulgcd  12007  rplpwr  12008  rppwr  12009  nnminle  12016  qredeq  12076  divgcdcoprmex  12082  cncongr1  12083  cncongr2  12084  dvdsnprmd  12105  euclemma  12126  prmexpb  12131  qnumdenbi  12172  eulerth  12213  fermltl  12214  prmdiv  12215  hashgcdlem  12218  odzcllem  12222  vfermltl  12231  reumodprminv  12233  modprm0  12234  modprmn0modprm0  12236  coprimeprodsq  12237  pythagtriplem1  12245  pythagtriplem3  12247  pythagtriplem4  12248  pythagtriplem10  12249  pythagtriplem6  12250  pythagtriplem7  12251  pythagtriplem8  12252  pythagtriplem9  12253  pythagtriplem11  12254  pythagtriplem12  12255  pythagtriplem13  12256  pythagtriplem14  12257  pythagtriplem15  12258  pythagtriplem16  12259  pythagtriplem17  12260  pythagtriplem19  12262  pythagtrip  12263  pcpremul  12273  pcdvdsb  12299  dvdsprmpweqnn  12315  dvdsprmpweqle  12316  difsqpwdvds  12317  pcfaclem  12327  pcbc  12329  unennn  12378  nninfdc  12434  setsex  12474  plusfvalg  12671  insubm  12759  grpidrcan  12821  grpidlcan  12822  grpsubpropd2  12861  mulgnnsubcl  12881  mulgnn0subcl  12882  mulgsubcl  12883  mulgaddcom  12892  mulginvcom  12893  mulgnnass  12903  mulgassr  12906  mulgpropdg  12910  ablinvadd  12937  ablsub4  12940  abladdsub4  12941  subcmnd  12953  srgcl  12976  srg1zr  12993  srgen1zr  12994  ringcl  13019  crngcom  13020  ringidss  13035  mulgass2  13058  opprmulg  13065  unitmulclb  13105  unitdvcl  13127  basgen  13240  2basgeng  13242  iuncld  13275  neipsm  13314  opnneissb  13315  opnssneib  13316  iscnp3  13363  cnprcl2k  13366  cnpnei  13379  cncnp2m  13391  cnptoprest  13399  sslm  13407  upxp  13432  cnmpt22  13454  distspace  13495  0met  13544  blvalps  13548  blval  13549  ssblps  13585  ssbl  13586  blpnfctr  13599  blopn  13650  blnei  13652  bdxmet  13661  bdbl  13663  metcnp3  13671  tgqioo  13707  ptolemy  13905  sinq12gt0  13911  sincosq1eq  13920  rpcxpadd  13986  cxpmul  13993  rplogbval  14023  logbleb  14039  logbgcd1irr  14045  logbprmirr  14050  lgsfvalg  14066  lgsneg1  14086  lgssq  14101  lgsdinn0  14109  bdfind  14347
  Copyright terms: Public domain W3C validator