Theorem pm3.27bi 326

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	biimp 151	. 2 |- (ph -> (ps /\ ch))
3	2	pm3.27d 325	1 |- (ph -> ch)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  sb1 1178  eumo 1413  2eu1 1452  eldifn 2166  unimax 2536  ssintub 2555  opth2 2806  pwssun 2833  weso 2946  ordwe 2967  onminsb 3015  onminesb 3016  tfis 3133  limomss 3143  ordom 3147  ssnlim 3173  funmo 3538  funss 3540  funeu 3543  funopg 3553  funco 3556  funun 3560  fununi 3569  funimaexg 3581  fndm 3593  fnopabg 3621  frn 3639  forn 3680  f1o2 3699  f1f1orn 3705  f1orescnv 3710  f1imacnv 3711  f1ococnv2 3714  dff3 3824  exfo 3828  f1fveq 3882  f1ofveu 3888  isorel 3900  tz7.48lem 3961  foprcl 4021  curry1 4104  eceqopreq 4319  sdomnen 4393  en0 4429  en1 4432  fodomr 4489  mapenlem1 4495  mapunen 4508  phplem4 4517  php3 4521  php3OLD 4522  fodomfi 4575  fodomfiOLD 4576  inf3lem2 4623  inf3lem6 4627  inf3lem7 4628  oancom 4642  tz9.12lem3 4671  rankr1 4684  scottex 4726  aceq5lem4 4748  aceq5lem5 4749  ac6 4765  kmlem1 4775  kmlem11 4785  zorn2lem2 4799  zorn 4807  brdom3 4811  oncardid 4831  cardid 4838  ondomcard 4868  iscard3 4899  alephval2 4913  0npi 5022  mulcanpi 5039  nlt1pi 5045  prcdpq 5109  prnmax 5111  suppsr3 5236  add20 5614  nn0p1nnt 6177  nnm1nn0t 6178  uzwo4OLD 6212  rpgt0t 6287  0nrp 6294  seq1rn2 6322  seqzrn2 6557  sqrlem12 6685  caucvglem6 7162  mulc1cncf 7279  ivthlem6 7286  ruclem23 7533  neiint 7716  neips 7724  hausnei 7781  metxplem1 7823  metxplem2 7824  metxplem4 7830  metxp 7831  cmscvg 7944  xplmi 7970  bcthlem4 7999  bcthlem14 8009  ablcom 8099  subgabl 8119  nvvcop 8209  bncms 8521  hlph 8589  pilem2 8667  sinperlem2 8682  eff1i 8739  relogf1o 8752  hcaucvg 9048  hlimconv 9054  shaddclt 9080  shaddcltOLD 9081  shmulclt 9082  shmulcltOLD 9083  chlim 9099  chcompl 9110  occl 9176  projlem15 9195  projlem22 9202  projlem26 9206  choc1 9286  nmopret 9792  cnopct 9832  lnoplt 9833  unopt 9834  hmopt 9841  cnfnct 9849  lnfnlt 9850  hmopidmch 10074  hmopidmpj 10075  elpjidmt 10107  sthil 10156  stjt 10157  mdslle1 10239  mdslle2 10240  atcv0 10264  chpssat 10285

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

Copyright terms: Public domain