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

Theorem 3expa 1139
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 1138 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 252 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  3anidm23  1229  mp3an2  1257  mpd3an3  1270  rgen3  2449  moi2  2774  sbc3ie  2888  preq12bg  3567  issod  4076  wepo  4116  reuhypd  4223  funimass4  5250  fvtp1g  5395  f1imass  5439  fcof1o  5454  f1ofveu  5525  f1ocnvfv3  5526  acexmid  5536  2ndrn  5834  frecrdg  6051  findcard  6412  findcard2  6413  findcard2s  6414  ltapig  6579  ltanqi  6643  ltmnqi  6644  lt2addnq  6645  lt2mulnq  6646  prarloclemcalc  6743  genpassl  6765  genpassu  6766  prmuloc  6807  ltexprlemm  6841  ltexprlemfl  6850  ltexprlemfu  6852  lteupri  6858  ltaprg  6860  mul4  7296  add4  7325  cnegexlem2  7340  cnegexlem3  7341  2addsub  7378  addsubeq4  7379  muladd  7544  ltleadd  7606  reapmul1  7751  apreim  7759  receuap  7815  p1le  7983  lemul12b  7995  lbinf  8082  zdiv  8505  fzind  8532  fnn0ind  8533  uzss  8709  qmulcl  8792  qreccl  8797  xrlttr  8935  icc0r  9014  iooshf  9040  elfz5  9102  elfz0fzfz0  9203  fzind2  9314  ioo0  9335  ico0  9337  ioc0  9338  expnegap0  9570  expineg2  9571  mulexpzap  9602  expsubap  9610  expnbnd  9682  facndiv  9752  bccmpl  9767  ibcval5  9776  bcpasc  9779  crim  9872  climshftlemg  10268  dvdsval3  10333  dvdsnegb  10346  muldvds1  10354  muldvds2  10355  dvdscmul  10356  dvdsmulc  10357  dvds2ln  10362  divalgb  10458  ndvdssub  10463  gcddiv  10541  rpexp1i  10666
  Copyright terms: Public domain W3C validator