Theorem 3imp 825

Description: Importation inference.

Hypothesis

Ref	Expression
3imp.1	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
3imp	|- ((ph /\ ps /\ ch) -> th)

Proof of Theorem 3imp

Step	Hyp	Ref	Expression
1		df-3an 775	. 2 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		3imp.1	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	imp31 362	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	1, 3	sylbi 199	1 |- ((ph /\ ps /\ ch) -> th)

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

This theorem is referenced by:  3impa 826  3impb 827  3impia 828  3impib 829  3com12 835  3com23 837  3an1rs 843  3imp1 844  3impd 845  syl3an2 858  syl3an3 859  3jao 883  vtocl3ga 1845  moi 1915  wefrc 2933  fvco2 3760  oawordri 4168  odi 4194  omass 4195  eceqopreq 4297  fodomr 4463  addsubt 5356  ltdiv2t 5835  squeeze0 5872  infmsup 6015  supxrun 6032  monoord 6231  expne0it 6519  expgt0t 6520  expge0t 6522  expgt1t 6523  mulexpt 6525  recexpt 6526  expaddt 6527  expmult 6528  bernneq 6583  facdivt 6879  climsqueeze 7076  climsqueeze2 7077  fsum0diag3 7195  infpnlem1 7449  tg2t 7563  tgss2t 7579  opnneissb 7669  cnpco 7708  metge0 7760  blss 7793  opni 7804  metcnp 7826  metcn4i 7906  bcthlem33 7965  ring2 8086  psasym 8576  chcompl 9036  spansncol 9407  pjoi0t 9579  hoaddsubt 9659  and4as 10332  fiiu 10350  fiv 10374  hmeogrp 10425  filintf 10443  fisub 10447  efilcp2 10450  cnfilca 10451  cmpassoh 10573  imonclem 10583  ismonc 10584  cmpmon 10585  icmpmon 10587

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