Theorem biimpa 416

Description: Inference from a logical equivalence.

Hypothesis

Ref	Expression
biimpa.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
biimpa	|- ((ph /\ ps) -> ch)

Proof of Theorem biimpa

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimpd 153	. 2 |- (ph -> (ps -> ch))
3	2	imp 350	1 |- ((ph /\ ps) -> ch)

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

This theorem is referenced by:  pm3.26bda 420  pm3.27bda 421  pm5.1 674  biimp3a 916  sb5rf 1254  euor 1391  cgsexg 1822  cgsex2g 1823  cgsex4g 1824  ceqsex 1825  sbciegft 1949  ifboth 2365  elpwunsn 2902  limsssuc 3111  opelxp1 3195  relop 3265  resiexg 3380  fnbr 3576  f1o00 3699  tz7.44lem1 3912  oev2 4146  oesuc 4150  oecl 4156  omordi 4181  omwordri 4187  omword2 4189  omordlim 4192  omlimcl 4193  oeordi 4198  oewordri 4203  oelim2 4206  en3d 4382  pw2en 4426  fodomr 4463  mapunen 4482  onomeneq 4498  r1ord 4627  rankr1 4646  alephfp 4872  cfeq0 4886  nlt1pi 5005  indpi 5006  ltrpq 5057  addgt0sr 5185  cnegext 5320  leltnet 5494  xrleltnet 5531  addge0 5573  ne0gt0t 5593  muln0t 5667  divdivdivt 5741  ltmul12it 5797  recgt1it 5848  nn2get 5890  supxr 6028  supxr2 6029  flge0nn0t 6185  flge1nnt 6186  seq1m1 6256  eluzp1m1t 6365  eluzaddi 6368  eluzsubi 6369  elfzuz2t 6418  fsequb2 6456  expsubt 6529  expordit 6531  expord2t 6535  exple1t 6538  expubndt 6539  sqlecant 6572  bernneq 6583  bernneq2 6584  expnbndt 6585  cvg2 6859  facwordit 6881  faclbnd4lem4 6888  bcval4t 6899  fsumsplit 6958  fsumrev 6967  fsumshft 6969  fsumcmpndx2 6980  fsumabs 6981  clm4le 7019  clm0i 7027  climge0 7049  climmullem1 7056  climmullem3 7058  climmullem4 7059  iserzex 7082  caucvg 7099  serzf0 7105  ser1f0 7106  ser1cmp 7110  ser1cmp2 7113  reccnv 7153  efcltlem1 7246  sin02gt0 7420  unbenlem 7447  elcls 7646  clsndisj 7648  unnei 7676  neissex 7679  metxptval 7770  metxpfval 7771  blss 7793  ssblex 7796  metcn 7828  metcnpi3 7831  metcnpi4 7832  metcni2 7834  tgioolem 7853  lmuni 7886  lmle 7895  cmsss 7931  bcthlem7 7939  bcthlem9 7941  bcthlem13 7945  bcthlem14 7946  bcthlem15 7947  bcthlem16 7948  bcthlem18 7950  bcthlem19 7951  bcthlem20 7952  vcoprnelem 8135  cnnv 8245  nvelbl 8263  nvcnpi4 8355  nmlnogt0 8389  nmblolbii 8390  blocnilem 8395  ajmoi 8450  ubthlem10 8469  pilem1 8590  sinq12gt0t 8625  efifolem7 8643  efif1lem1 8645  shftefif1olem 8661  shftefif1olemOLD 8662  eff1i 8665  effoi 8666  effoiOLD 8667  hhnv 8953  norm1t 9042  hhssnv 9054  pjthlem10 9143  pjspansnt 9417  spanunsn 9419  fh1t 9478  fh2t 9479  cm2jt 9480  pjidt 9557  adjmo 9675  eleigvecclt 9799  eigvalclt 9801  eigvect 9802  eighmret 9803  eighmortht 9804  nmop0h 9831  nmbdoplb 9864  nmcopexlem5 9870  nmcoplb 9873  nmophm 9876  lnopcon 9878  lncnopbd 9881  nmbdfnlb 9893  nmcfnexlem5 9899  nmcfnlb 9902  lnfncon 9905  cnlnadjeu 9925  branmfnt 9951  rnbra 9953  nmopleidt 9983  strlem5 10092  hstrlem5 10100  dmdbr3 10141  dmdbr4 10142  mdsl3t 10151  hatomistic 10197  cvexchlem 10203  irredlem1 10225  irredlem2 10226  irred 10229  atcvat3 10231  atcvat4 10232  atabs 10236  mdsymlem1 10238  mdsymlem3 10240  mdsymlem5 10242  dmdbr5at 10255  cdj1 10265  uninqs 10342  cdrci 10381  hmeomap 10405  hmeocna 10406  hmeocnb 10407  fipfil2 10439  neifil 10442  mslb1 10473  ehm 10563  dehm 10564  cehm 10565

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