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

Theorem 3expa 1182
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3expa (((𝜑𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3expa
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1181 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 254 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 963
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 965
This theorem is referenced by:  ad4ant123  1194  ad4ant124  1195  ad4ant134  1196  ad4ant234  1197  3anidm23  1276  mp3an2  1304  mpd3an3  1317  rgen3  2522  moi2  2868  sbc3ie  2985  preq12bg  3707  issod  4248  wepo  4288  reuhypd  4399  funimass4  5479  fvtp1g  5635  f1imass  5682  fcof1o  5697  f1ofveu  5769  f1ocnvfv3  5770  acexmid  5780  2ndrn  6088  frecrdg  6312  oawordriexmid  6373  mapxpen  6749  findcard  6789  findcard2  6790  findcard2s  6791  ltapig  7169  ltanqi  7233  ltmnqi  7234  lt2addnq  7235  lt2mulnq  7236  prarloclemcalc  7333  genpassl  7355  genpassu  7356  prmuloc  7397  ltexprlemm  7431  ltexprlemfl  7440  ltexprlemfu  7442  lteupri  7448  ltaprg  7450  mul4  7917  add4  7946  cnegexlem2  7961  cnegexlem3  7962  2addsub  7999  addsubeq4  8000  muladd  8169  ltleadd  8231  reapmul1  8380  apreim  8388  receuap  8453  p1le  8630  lemul12b  8642  lbinf  8729  zdiv  9162  fzind  9189  fnn0ind  9190  uzss  9369  qmulcl  9455  qreccl  9460  xrlttr  9610  xaddass  9681  icc0r  9738  iooshf  9764  elfz5  9828  elfz0fzfz0  9933  fzind2  10046  ioo0  10067  ico0  10069  ioc0  10070  expnegap0  10331  expineg2  10332  mulexpzap  10363  expsubap  10371  expnbnd  10445  facndiv  10516  bccmpl  10531  bcval5  10540  bcpasc  10543  crim  10661  climshftlemg  11102  2sumeq2dv  11171  hash2iun  11279  2cprodeq2dv  11368  dvdsval3  11531  dvdsnegb  11544  muldvds1  11552  muldvds2  11553  dvdscmul  11554  dvdsmulc  11555  dvds2ln  11560  divalgb  11656  ndvdssub  11661  gcddiv  11741  rpexp1i  11866  phiprmpw  11932  hashgcdeq  11938  innei  12369  iscnp4  12424  cnpnei  12425  cnnei  12438  cnconst  12440  ismeti  12552  isxmet2d  12554  elbl2ps  12598  elbl2  12599  xblpnfps  12604  xblpnf  12605  xblm  12623  blininf  12630  blssexps  12635  blssex  12636  blsscls2  12699  metss  12700  metrest  12712  metcn  12720  divcnap  12761  cdivcncfap  12793
  Copyright terms: Public domain W3C validator