Theorem pm3.27bi 324

Description: Deduction eliminating a conjunct.

Hypothesis

Ref	Expression
pm3.27bi.1	|- (ph <-> (ps /\ ch))

Assertion

Ref	Expression
pm3.27bi	|- (ph -> ch)

Proof of Theorem pm3.27bi

Step	Hyp	Ref	Expression
1		pm3.27bi.1	. . 3 |- (ph <-> (ps /\ ch))
2	1	biimpi 149	. 2 |- (ph -> (ps /\ ch))
3	2	pm3.27d 323	1 |- (ph -> ch)

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221

This theorem is referenced by:  sb1 1213  eumo 1450  2eu1 1489  eldifn 2215  unimax 2599  ssintub 2618  opth2 2876  pwssun 2905  weso 2967  ordwe 2988  onminsb 3155  onminesb 3156  tfis 3208  limomss 3224  ordom 3228  ssnlim 3236  funmo 3637  funss 3639  funeu 3642  funopg 3652  funco 3655  funun 3659  fununi 3668  funimaexg 3681  fndm 3693  fnopabg 3722  frn 3740  forn 3782  dff1o2 3801  f1f1orn 3807  f1orescnv 3812  f1imacnv 3813  f1ococnv2 3819  dff4 3932  exfo 3936  f1fveq 3990  f1ofveu 3996  isorel 4008  foprcl 4075  curry1 4193  curry2 4196  tz7.48lem 4256  eceqopreq 4454  sdomnen 4528  en0 4564  en1 4567  fodomr 4628  mapenlem1 4636  mapunen 4649  phplem4 4658  php3 4662  fodomfi 4709  inf3lem2 4759  inf3lem6 4763  inf3lem7 4764  oancom 4779  tz9.12lem3 4807  rankr1 4820  scottex 4862  aceq5lem4 4884  aceq5lem5 4885  ac6 4901  kmlem1 4911  kmlem11 4921  zorn2lem2 4935  zorn 4943  brdom3 4947  oncardid 4967  cardid 4975  ondomcard 5007  iscard3 5038  alephval2 5052  0npi 5164  mulcanpi 5181  nlt1pi 5187  prcdpq 5251  prnmax 5253  suppsr3 5378  add20i 5756  rpgt0 6199  0nrp 6212  nn0p1nn 6343  nnm1nn0 6344  uzwo4OLD 6381  seq1rn2 6686  seqzrn2 6751  sqrlem12 6885  caucvglem6 7365  mulc1cncf 7484  ivthlem6 7491  ruclem23 7744  neiint 7929  neips 7937  hausnei 7994  metxplem1 8036  metxplem2 8037  metxplem4 8043  metxp 8044  cmscvg 8158  xplmi 8184  bcthlem4 8213  bcthlem14 8223  gxneg 8322  gxsuc 8328  gxadd 8331  gxmul 8334  ablcom 8344  subgabl 8365  nvvcop 8460  bncms 8782  hlph 8853  pilem2 8939  sinperlem2 8954  eff1i 9016  relogf1o 9029  hcaucvg 9329  hlimconvi 9335  shaddcl 9361  shaddclOLD 9362  shmulcl 9363  shmulclOLD 9364  chlimi 9380  chcompl 9391  occli 9457  projlem15 9476  projlem22 9483  projlem26 9487  choc1 9567  nmopre 10077  cnopc 10117  lnopl 10118  unop 10119  hmop 10126  cnfnc 10134  lnfnl 10135  hmopidmchi 10359  hmopidmpji 10360  elpjidm 10392  sthil 10442  stj 10443  mdslle1i 10525  mdslle2i 10526  atcv0 10550  chpssati 10571  smgrpisass 10910  mndisexid 10922  ordtypelem2 11428  hartoglem 11435  omsubsdom 11442  infenomsub 11450  compcov 11486  uncomp 11490  alexsub 11500  reconnlem5 11511  2ndccb 11536  refssfne 11565  locfincomp 11575  t0dist 11602  t1sncld 11606  regsep 11611  nrmsep 11615  fbssint 11626  ufilss 11652  ufilmax 11653  fcluscf 11724  flimfnfcls 11727  gapmlem 11783  cnvcan 11814  indexa 11845  hmeocld 11961  txcn 11979  heiborlem1 12011  heiborlem22 12032  heiborlem36 12046  heiborlem39 12049  heiborlem42 12052

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 145  df-an 223

Copyright terms: Public domain