Theorem 3imp 829

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

This theorem is referenced by:  3impa 830  3impb 831  3impia 832  3impib 833  3com12 839  3com23 841  3an1rs 847  3imp1 848  3impd 849  syl3an2 862  syl3an3 863  3jao 888  vtocl3ga 1857  moi 1928  wefrc 2949  fvco2 3781  oawordri 4190  odi 4216  omass 4217  eceqopreq 4319  fodomr 4489  addsubt 5396  mulcant 5702  divdirt 5757  ltdiv1t 5851  ltmuldivt 5865  ltdiv2t 5889  squeeze0 5926  infmsup 6070  supxrun 6087  monoord 6295  expne0it 6589  expgt0t 6590  expge0t 6592  expgt1t 6593  mulexpt 6595  recexpt 6596  expaddt 6597  expmult 6598  bernneq 6653  facdivt 6942  climsqueeze 7140  climsqueeze2 7141  fsum0diag3 7260  infpnlem1 7507  tg2t 7620  tgss2t 7636  opnneissb 7725  cnpco 7766  metge0 7816  blss 7850  opni 7861  metcnp 7884  metcn4i 7969  bcthlem33 8028  ring2 8145  psasym 8647  pstr 8648  chcompl 9110  spansncol 9486  pjoi0t 9657  hoaddsubt 9737  and4as 10427  fiiu 10444  fiv 10470  hmeogrp 10524  hmeobc 10528  unpde2eg2 10530  homindlem3 10537  filintf 10554  fisub 10558  efilcp2 10561  cnfilca 10562  rcfpfillem2 10564  rcfpfillem6 10568  cmpassoh 10700  imonclem 10712  ismonc 10713  cmpmon 10714  icmpmon 10715

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 779

Copyright terms: Public domain