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

Theorem 3ad2ant1 1002
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1  |-  ( ph  ->  ch )
Assertion
Ref Expression
3ad2ant1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )

Proof of Theorem 3ad2ant1
StepHypRef Expression
1 3ad2ant.1 . . 3  |-  ( ph  ->  ch )
21adantr 274 . 2  |-  ( (
ph  /\  th )  ->  ch )
323adant2 1000 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
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  7260  prltlu  7302  prarloclem3step  7311  prarloclem5  7315  ltasrg  7585  cnegexlem1  7944  addcan  7949  apcotr  8376  apadd1  8377  mulext1  8381  divdivap1  8490  divdivap2  8491  div2negap  8502  divneg2ap  8503  ltmulgt11  8629  ltdiv2  8652  squeeze0  8669  nndivtr  8769  nn0n0n1ge2  9128  zdivmul  9148  gtndiv  9153  eluzuzle  9341  eluzp1p1  9358  qdivcl  9442  irrmul  9446  rpgecl  9477  xaddass  9659  xltadd1  9666  xlt2add  9670  lbico1  9720  lbicc2  9774  zltaddlt1le  9796  uzsubsubfz  9834  elfz1b  9877  elfz0ubfz0  9909  fz0fzelfz0  9911  difelfzle  9918  difelfznle  9919  2ffzeq  9925  fzo1fzo0n0  9967  ubmelfzo  9984  fzonn0p1p1  9997  elfzom1p1elfzo  9998  elfzonelfzo  10014  subfzo0  10026  ceiqle  10093  ceilqle  10094  modqval  10104  flqpmodeq  10107  modq0  10109  negqmod0  10111  modqge0  10112  modqlt  10113  modqdiffl  10115  modqmulnn  10122  modqvalp1  10123  modqmuladdnn0  10148  qnegmod  10149  addmodid  10152  modfzo0difsn  10175  addmodlteq  10178  qexpclz  10321  expgt1  10338  expp1zap  10349  expm1ap  10350  expubnd  10357  bernneq2  10420  expnlbnd  10423  omgadd  10555  hashun  10558  fihashssdif  10571  hashdifpr  10573  fimaxq  10580  shftuz  10596  mulreap  10643  redivap  10653  imdivap  10660  resqrtcl  10808  xrmaxltsup  11034  xrmaxaddlem  11036  xrmaxadd  11037  xrlemininf  11047  xrminltinf  11048  climuni  11069  addcn2  11086  mulcn2  11088  efsub  11394  sin02gt0  11477  cos12dec  11481  dvdsval2  11503  addmodlteqALT  11564  modremain  11633  fldivndvdslt  11639  mulgcdr  11713  gcddiv  11714  rpmulgcd  11721  rplpwr  11722  rppwr  11723  qredeq  11784  divgcdcoprmex  11790  cncongr1  11791  cncongr2  11792  dvdsnprmd  11813  euclemma  11831  prmexpb  11836  qnumdenbi  11877  hashgcdlem  11910  unennn  11917  setsex  12001  basgen  12259  2basgeng  12261  iuncld  12294  neipsm  12333  opnneissb  12334  opnssneib  12335  iscnp3  12382  cnprcl2k  12385  cnpnei  12398  cncnp2m  12410  cnptoprest  12418  sslm  12426  upxp  12451  cnmpt22  12473  distspace  12514  0met  12563  blvalps  12567  blval  12568  ssblps  12604  ssbl  12605  blpnfctr  12618  blopn  12669  blnei  12671  bdxmet  12680  bdbl  12682  metcnp3  12690  tgqioo  12726  ptolemy  12918  sinq12gt0  12924  sincosq1eq  12933  bdfind  13174
  Copyright terms: Public domain W3C validator