Theorem 3expia 834

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

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 831	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp 350	1 |- ((ph /\ ps) -> (ch -> th))

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 774

This theorem is referenced by:  3gencl 1827  nnsuc 3144  tfinds 3157  3optocl 3233  ndmord 4045  curry1val 4093  elrnoprabg 4117  eceqopreq 4306  mapvalg 4323  pmvalg 4324  axsup 5490  ltlent 5505  recext 5667  ltdivmult 5829  ledivmult 5830  nndivt 5916  supxrgtmnf 6049  zextltt 6147  primet 6152  uzind2 6164  qbtwnxr 6229  ioo0t 6318  iccssret 6342  fznt 6438  expge0t 6536  expge1t 6538  expordit 6545  exple1t 6552  clim2serzt 7087  serzf0 7122  ser1f0 7123  ser1cmp2lem 7129  isummulc1 7164  efaddlem25 7321  reeftlclt 7339  znnenlem 7460  bastop 7602  qdensere 7711  cncnpi 7733  cncnp 7738  cncnp2 7739  ishausi 7745  metcn 7851  metcnpi3 7854  metcnpi4 7855  metcni2 7857  cncfmet 7867  blssioo 7875  metelcls 7927  metcnp4 7932  iscms2lem5 7955  grplactf1o 8061  ring2 8113  nmobndi 8398  ipasslem5 8453  spwnex 8618  efifolem4 8675  efifolem5 8676  efifolem6 8677  omlsi 9200  spansneleq 9449  spansneleqOLD 9450  elspansn4t 9453  homco1t 9684  homulasst 9685  homco2t 9858  mdsl0 10193  ssdmd1 10196  ssdmd2 10197  cvdmdt 10220  irredlem2 10274  atdmd 10281  atmd2 10283  ghomf1olem 10352  cayleylem2 10366  ee7.2a 10383  elioo1t3 10442  cmphmp 10467  homcard 10485  dtt2 10534  cmpassoh 10645  fmamo 10666  vidfunid 10667  iddvvidd 10668  idcvvidc 10669

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 776

Copyright terms: Public domain