HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem 3expia 833
Description: Exportation from triple conjunction.
Hypothesis
Ref Expression
3exp.1 |- ((ph /\ ps /\ ch) -> th)
Assertion
Ref Expression
3expia |- ((ph /\ ps) -> (ch -> th))
Proof of Theorem 3expia
StepHypRef Expression
1 3exp.1 . . 3 |- ((ph /\ ps /\ ch) -> th)
213exp 830 . 2 |- (ph -> (ps -> (ch -> th)))
32imp 350 1 |- ((ph /\ ps) -> (ch -> th))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 773
This theorem is referenced by:  3gencl 1821  nnsuc 3138  tfinds 3151  3optocl 3227  ndmord 4036  curry1val 4084  elrnoprabg 4108  eceqopreq 4297  mapvalg 4314  pmvalg 4315  axsup 5479  ltlent 5495  recext 5657  ltdivmult 5819  ledivmult 5820  nndivt 5906  supxrgtmnf 6039  zextltt 6137  primet 6142  uzind2 6154  qbtwnxr 6217  ioo0t 6305  iccssret 6329  fznt 6425  expge0t 6522  expge1t 6524  expordit 6531  exple1t 6538  clim2serzt 7070  serzf0 7105  ser1f0 7106  ser1cmp2lem 7112  isummulc1 7147  efaddlem25 7304  reeftlclt 7322  znnenlem 7443  bastop 7584  qdensere 7691  cncnpi 7712  cncnp 7717  cncnp2 7718  ishausi 7724  metcn 7828  metcnpi3 7831  metcnpi4 7832  metcni2 7834  cncfmet 7844  blssioo 7852  metelcls 7900  metcnp4 7904  iscms2lem5 7927  grplactf1o 8034  ring2 8086  nmobndi 8370  ipasslem5 8425  efifolem4 8640  efifolem5 8641  efifolem6 8642  omlsi 9160  spansneleq 9409  spansneleqOLD 9410  elspansn4t 9413  homco1t 9644  homulasst 9645  homco2t 9817  mdsl0 10145  ssdmd1 10148  ssdmd2 10149  cvdmdt 10172  irredlem2 10226  atdmd 10233  atmd2 10235  ghomf1olem 10301  cayleylem2 10317  elioo1t3 10383  cmphmp 10408  homcard 10426  dtt2 10462  cmpassoh 10573  fmamo 10594  vidfunid 10595  iddvvidd 10596  idcvvidc 10597
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 775
Copyright terms: Public domain