Theorem 3imp 1061

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 860	. 2 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		3imp.1	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	imp31 389	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	1, 3	sylbi 216	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  3impa 1062  3impb 1063  3impia 1064  3impib 1065  3com12OLD 1072  3com23 1074  3an1rs 1080  3imp1 1081  3impd 1082  syl3an2 1131  syl3an3 1132  3jao 1158  ee333 1279  vtocl3ga 2354  vtoclegft 2356  moi 2436  wefrc 3652  fvco2OLD 4738  oawordri 5232  odi 5258  omass 5259  eceqopreq 5372  addsubOLD 6543  mulcan 6880  divmul 6896  divdir 6933  ltmul1 7008  lemul1OLD 7012  ltdiv1 7031  ltmuldiv 7045  ltdiv2 7070  squeeze0 7107  infmsup 7277  supxrun 7294  monoord 7523  expgt0 7831  expge0 7833  expgt1 7834  mulexp 7836  exprecOLD 7838  expadd 7839  expmul 7840  bernneq 7898  bernneqOLD 7899  facdiv 8194  climsqueeze 8400  climsqueeze2 8401  fsum0diag3 8522  infpnlem1 8775  tg2 8891  tgss2 8907  opnneissb 9004  cnpco 9046  metge0 9096  blss 9130  opni 9141  metequiv 9158  metcnp 9165  metcn4i 9250  bcthlem33 9309  gafo 9451  gaid 9454  ring2 9474  cardennn 10171  indexfi 10174  findcardOLD 10179  fiv 10212  hausnei2 10222  hmeobc 10239  issubspt 10247  filintf 10274  elfilmap 10312  hausfillim2 10325  clmgm 10368  ismnd2 10392  grpmnd 10393  on1el3 10412  chcompl 10748  spansncol 11124  hoaddsub 11379  funpsstri 13835  predso 13895  tz6.26 13913  poxp 13949  and4as 14266  fiiu 14344  isunscov 14386  unpde2eg2 14406  infxpg 14422  eqfnung2 14459  injrec 14461  surjsec 14462  surjsec2 14467  mapmapmap 14486  npincppr 14501  prjnpl 14510  unprj 14511  prl 14512  prl2 14514  prjmapcp2 14515  iscst2 14520  pre2befi2 14573  preotr2 14576  prltub 14602  dfps2 14634  tostos 14637  fprod1s1 14679  fprodp1s1 14683  fprod1i2 14685  iscomb 14690  clfsebs 14707  clfsebsr 14709  fincmpzer 14711  fprodadd 14713  fprodneg 14741  fprodsub 14742  multinv 14771  multinvb 14772  zerdivemp1 14785  rngridfz 14786  sum2vv 14805  svs2 14829  truni3 14851  unint2t 14866  mapdiscn 14871  hmeogrp 14892  homindlem3 14900  fisub 14924  efilcp2 14926  cnfilca 14927  rcfpfillem2 14929  rcfpfillem6 14933  limfilnei 14943  conttnf 14944  iscnp3 14946  bwt2 14960  tpgprop1 14986  flimfneicn 15037  lvsovso 15038  lvsovso2 15039  dualcat2lem 15129  dualded2lem 15130  dualalg 15131  dualcat2 15133  cmpassoh 15150  imonclem 15162  ismonc 15163  cmpmon 15164  icmpmon 15165  iepiclem 15172  isepic 15173  issubcat 15193  idsubfun 15206  tarax3f 15229  tarcrpr 15237  tartrel 15239  tartord 15240  cptarc 15242  tarsuc3 15246  intrtael 15256  tartarmap 15265  efp2 15290  imp5p 15348  compsublem 15430  compsub 15431  reconn 15451  topmtcl 15525  ufprim 15569  filufint 15574  indexfiOLD 15755  totbndss 15937  heiborlem23 15977  rrnmet 16016  ringneglmul 16104  ringnegrmul 16105  zerdivemp1x 16108  e333 16601  joinle 16820  meetle 16827  clatleglb 16903  atlatex 17013  hlexch 17034  pmaple 17241

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 164  df-an 242  df-3an 860

Copyright terms: Public domain