Theorem 3imp 827

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 777	. 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 775

This theorem is referenced by:  3impa 828  3impb 829  3impia 830  3impib 831  3com12 837  3com23 839  3an1rs 845  3imp1 846  3impd 847  syl3an2 860  syl3an3 861  3jao 886  vtocl3ga 1854  moi 1925  wefrc 2943  fvco2 3775  oawordri 4184  odi 4210  omass 4211  eceqopreq 4313  fodomr 4483  addsubt 5384  mulcant 5690  divdirt 5750  ltdiv1t 5849  ltmuldivt 5863  ltdiv2t 5887  squeeze0 5924  infmsup 6068  supxrun 6085  monoord 6294  expne0it 6588  expgt0t 6589  expge0t 6591  expgt1t 6592  mulexpt 6594  recexpt 6595  expaddt 6596  expmult 6597  bernneq 6652  facdivt 6942  climsqueeze 7140  climsqueeze2 7141  fsum0diag3 7260  infpnlem1 7506  tg2t 7621  tgss2t 7637  opnneissb 7728  cnpco 7769  metge0 7819  blss 7853  opni 7864  metcnp 7887  metcn4i 7972  bcthlem33 8031  ring2 8149  psasym 8651  pstr 8652  chcompl 9115  spansncol 9491  pjoi0t 9662  hoaddsubt 9742  and4as 10432  fiiu 10453  fiiuOLD 10454  fiv 10482  fivOLD 10483  hmeogrp 10538  hmeobc 10542  sfseqeq 10543  unpde2eg2 10544  homindlem3 10551  filintf 10569  fisub 10576  fisubOLD 10577  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem2 10587  rcfpfillem2OLD 10588  rcfpfillem6 10595  rcfpfillem6OLD 10596  cmpassoh 10729  imonclem 10741  ismonc 10742  cmpmon 10743  icmpmon 10744

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 777

Copyright terms: Public domain