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  8337  apadd1  8338  mulext1  8342  divdivap1  8451  divdivap2  8452  div2negap  8463  divneg2ap  8464  ltmulgt11  8590  ltdiv2  8613  squeeze0  8630  nndivtr  8730  nn0n0n1ge2  9089  zdivmul  9109  gtndiv  9114  eluzuzle  9302  eluzp1p1  9319  qdivcl  9403  irrmul  9407  rpgecl  9438  xaddass  9620  xltadd1  9627  xlt2add  9631  lbico1  9681  lbicc2  9735  zltaddlt1le  9757  uzsubsubfz  9795  elfz1b  9838  elfz0ubfz0  9870  fz0fzelfz0  9872  difelfzle  9879  difelfznle  9880  2ffzeq  9886  fzo1fzo0n0  9928  ubmelfzo  9945  fzonn0p1p1  9958  elfzom1p1elfzo  9959  elfzonelfzo  9975  subfzo0  9987  ceiqle  10054  ceilqle  10055  modqval  10065  flqpmodeq  10068  modq0  10070  negqmod0  10072  modqge0  10073  modqlt  10074  modqdiffl  10076  modqmulnn  10083  modqvalp1  10084  modqmuladdnn0  10109  qnegmod  10110  addmodid  10113  modfzo0difsn  10136  addmodlteq  10139  qexpclz  10282  expgt1  10299  expp1zap  10310  expm1ap  10311  expubnd  10318  bernneq2  10381  expnlbnd  10384  omgadd  10516  hashun  10519  fihashssdif  10532  hashdifpr  10534  fimaxq  10541  shftuz  10557  mulreap  10604  redivap  10614  imdivap  10621  resqrtcl  10769  xrmaxltsup  10995  xrmaxaddlem  10997  xrmaxadd  10998  xrlemininf  11008  xrminltinf  11009  climuni  11030  addcn2  11047  mulcn2  11049  efsub  11314  sin02gt0  11397  cos12dec  11401  dvdsval2  11423  addmodlteqALT  11484  modremain  11553  fldivndvdslt  11559  mulgcdr  11633  gcddiv  11634  rpmulgcd  11641  rplpwr  11642  rppwr  11643  qredeq  11704  divgcdcoprmex  11710  cncongr1  11711  cncongr2  11712  dvdsnprmd  11733  euclemma  11751  prmexpb  11756  qnumdenbi  11797  hashgcdlem  11830  unennn  11837  setsex  11918  basgen  12176  2basgeng  12178  iuncld  12211  neipsm  12250  opnneissb  12251  opnssneib  12252  iscnp3  12299  cnprcl2k  12302  cnpnei  12315  cncnp2m  12327  cnptoprest  12335  sslm  12343  upxp  12368  cnmpt22  12390  distspace  12431  0met  12480  blvalps  12484  blval  12485  ssblps  12521  ssbl  12522  blpnfctr  12535  blopn  12586  blnei  12588  bdxmet  12597  bdbl  12599  metcnp3  12607  tgqioo  12643  ptolemy  12832  sinq12gt0  12838  sincosq1eq  12847  bdfind  13071
  Copyright terms: Public domain W3C validator