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

Theorem 3expb 1182
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 1180 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 255 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  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:  3adant3r1  1190  3adant3r2  1191  3adant3r3  1192  3adant1l  1208  3adant1r  1209  mp3an1  1302  soinxp  4609  sotri  4934  fnfco  5297  mpoeq3dva  5835  fovrnda  5914  ovelrn  5919  grprinvd  5966  fnmpoovd  6112  nnmsucr  6384  fidifsnid  6765  exmidpw  6802  undiffi  6813  fidcenumlemim  6840  ltpopr  7417  ltexprlemdisj  7428  recexprlemdisj  7452  mul4  7908  add4  7937  2addsub  7990  addsubeq4  7991  subadd4  8020  muladd  8160  ltleadd  8222  divmulap  8449  divap0  8458  div23ap  8465  div12ap  8468  divsubdirap  8482  divcanap5  8488  divmuleqap  8491  divcanap6  8493  divdiv32ap  8494  div2subap  8610  letrp1  8620  lemul12b  8633  lediv1  8641  cju  8733  nndivre  8770  nndivtr  8776  nn0addge1  9037  nn0addge2  9038  peano2uz2  9172  uzind  9176  uzind3  9178  fzind  9180  fnn0ind  9181  uzind4  9397  qre  9431  irrmul  9453  rpdivcl  9481  rerpdivcl  9486  iccshftr  9791  iccshftl  9793  iccdil  9795  icccntr  9797  fzaddel  9853  fzrev  9878  frec2uzf1od  10193  expdivap  10358  2shfti  10617  iooinsup  11060  isermulc2  11123  dvds2add  11540  dvds2sub  11541  dvdstr  11543  alzdvds  11565  divalg2  11636  lcmgcdlem  11771  lcmgcdeq  11777  isprm6  11838  tgclb  12250  topbas  12252  neissex  12350  cnpnei  12404  txcnp  12456  psmetxrge0  12517  psmetlecl  12519  xmetlecl  12552  xmettpos  12555  elbl3ps  12579  elbl3  12580  metss  12679  comet  12684  bdxmet  12686  bdmet  12687  bl2ioo  12727  divcnap  12740  cncffvrn  12754  divccncfap  12762  dvrecap  12862  cosz12  12885
  Copyright terms: Public domain W3C validator