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

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

Proof of Theorem 3expb
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1140 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 253 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922
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 924
This theorem is referenced by:  3adant3r1  1150  3adant3r2  1151  3adant3r3  1152  3adant1l  1164  3adant1r  1165  mp3an1  1258  soinxp  4478  sotri  4796  fnfco  5151  mpt2eq3dva  5672  fovrnda  5747  ovelrn  5752  grprinvd  5799  nnmsucr  6205  fidifsnid  6541  exmidpw  6578  undiffi  6589  ltpopr  7101  ltexprlemdisj  7112  recexprlemdisj  7136  mul4  7561  add4  7590  2addsub  7643  addsubeq4  7644  subadd4  7673  muladd  7809  ltleadd  7871  divmulap  8084  divap0  8093  div23ap  8100  div12ap  8103  divsubdirap  8117  divcanap5  8123  divmuleqap  8126  divcanap6  8128  divdiv32ap  8129  letrp1  8247  lemul12b  8260  lediv1  8268  cju  8359  nndivre  8395  nndivtr  8401  nn0addge1  8655  nn0addge2  8656  peano2uz2  8789  uzind  8793  uzind3  8795  fzind  8797  fnn0ind  8798  uzind4  9011  qre  9045  irrmul  9067  rpdivcl  9094  rerpdivcl  9099  iccshftr  9346  iccshftl  9348  iccdil  9350  icccntr  9352  fzaddel  9407  fzrev  9431  frec2uzf1od  9744  expdivap  9926  2shfti  10183  iisermulc2  10644  dvds2add  10755  dvds2sub  10756  dvdstr  10758  alzdvds  10780  divalg2  10851  lcmgcdlem  10984  lcmgcdeq  10990  isprm6  11051
  Copyright terms: Public domain W3C validator