HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
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
StepHypRef Expression
1 pm3.27bi.1 . . 3 |- (ph <-> (ps /\ ch))
21biimp 151 . 2 |- (ph -> (ps /\ ch))
32pm3.27d 325 1 |- (ph -> ch)
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223
This theorem is referenced by:  sb1 1172  eumo 1404  2eu1 1442  eldifn 2153  unimax 2522  ssintub 2541  opth2 2789  pwssun 2816  weso 2930  ordwe 2951  onminsb 2999  onminesb 3000  tfis 3117  limomss 3127  ordom 3131  ssnlim 3157  funmo 3518  funss 3520  funeu 3523  funopg 3533  funco 3536  funun 3540  fununi 3549  funimaexg 3561  fndm 3573  fnopabg 3601  frn 3618  forn 3659  f1o2 3678  f1f1orn 3684  f1orescnv 3689  f1imacnv 3690  f1ococnv2 3693  dff3 3803  exfo 3807  f1fveq 3861  f1ofveu 3867  isorel 3879  tz7.48lem 3940  foprcl 4000  curry1 4082  eceqopreq 4297  sdomnen 4368  en0 4404  en1 4407  fodomr 4463  mapenlem1 4469  mapunen 4482  phplem4 4491  php3 4495  fodomfi 4540  inf3lem2 4586  inf3lem6 4590  inf3lem7 4591  oancom 4605  tz9.12lem3 4633  rankr1 4646  scottex 4688  aceq5lem4 4710  aceq5lem5 4711  ac6 4727  kmlem1 4737  kmlem11 4747  zorn2lem2 4761  zorn 4769  brdom3 4773  oncardid 4793  cardid 4800  ondomcard 4829  iscard3 4860  alephval2 4874  0npi 4982  mulcanpi 4999  nlt1pi 5005  prcdpq 5069  prnmax 5071  suppsr3 5196  add20 5576  nn0p1nnt 6122  nnm1nn0t 6123  uzwo4OLD 6158  rpgt0t 6224  0nrp 6230  seq1rn2 6258  seqzrn2 6488  sqrlem12 6614  caucvglem6 7098  mulc1cncf 7214  ivthlem6 7221  ivthlem6OLD 7230  ivthlem7OLD 7231  ruclem23 7475  neiint 7660  neips 7668  hausnei 7723  metxplem1 7766  metxplem2 7767  metxplem4 7773  metxp 7774  cmscvg 7882  xplmi 7907  bcthlem4 7936  bcthlem14 7946  ablcom 8039  subgabl 8060  nvvcop 8151  bncms 8456  hlph 8524  pilem2 8591  sinperlem2 8606  circgrpOLD 8658  eff1i 8665  relogf1o 8679  hcaucvg 8974  hlimconv 8980  shaddclt 9006  shaddcltOLD 9007  shmulclt 9008  shmulcltOLD 9009  chlim 9025  chcompl 9036  occl 9097  projlem15 9116  projlem22 9123  projlem26 9127  choc1 9206  nmopret 9714  cnopct 9753  lnoplt 9754  unopt 9755  hmopt 9762  cnfnct 9770  lnfnlt 9771  hmopidmch 9990  hmopidmpj 9991  elpjidmt 10022  sthil 10071  stjt 10072  mdslle1 10152  mdslle2 10153  atcv0 10177  chpssat 10198
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