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 675  biimp3a 917  sb5rf 1257  euor 1396  cgsexg 1827  cgsex2g 1828  cgsex4g 1829  ceqsex 1830  sbciegft 1955  ifboth 2371  elpwunsn 2907  limsssuc 3116  opelxp1 3200  relop 3270  resiexg 3388  fnbr 3582  f1o00 3705  tz7.44lem1 3918  oev2 4152  oesuc 4156  oecl 4162  omordi 4187  omwordri 4193  omword2 4195  omordlim 4198  omlimcl 4199  oeordi 4204  oewordri 4209  oelim2 4212  en3d 4388  pw2en 4432  fodomr 4469  mapunen 4488  onomeneq 4504  r1ord 4635  rankr1 4654  alephfp 4880  cfeq0 4894  nlt1pi 5013  indpi 5014  ltrpq 5065  addgt0sr 5193  cnegext 5328  leltnet 5502  xrleltnet 5539  addge0 5581  ne0gt0t 5601  muln0t 5675  divdivdivt 5749  ltmul12it 5805  recgt1it 5856  nn2get 5898  supxr 6036  supxr2 6037  flge0nn0t 6193  flge1nnt 6194  seq1m1 6264  eluzp1m1t 6373  eluzaddi 6376  eluzsubi 6377  elfzuz2t 6426  fsequb2 6464  expsubt 6537  expordit 6539  expord2t 6543  exple1t 6546  expubndt 6547  sqlecant 6580  bernneq 6591  bernneq2 6592  expnbndt 6593  cvg2 6867  facwordit 6889  faclbnd4lem4 6896  bcval4t 6907  fsumsplit 6966  fsumrev 6975  fsumshft 6977  fsumcmpndx2 6988  fsumabs 6989  clm4le 7027  clm0i 7035  climge0 7057  climmullem1 7064  climmullem3 7066  climmullem4 7067  iserzex 7090  caucvg 7107  serzf0 7113  ser1f0 7114  ser1cmp 7118  ser1cmp2 7121  reccnv 7161  efcltlem1 7254  sin02gt0 7428  unbenlem 7455  elcls 7654  clsndisj 7656  unnei 7685  neissex 7688  metxptval 7782  metxpfval 7783  blss 7805  ssblex 7808  metcn 7841  metcnpi3 7844  metcnpi4 7845  metcni2 7847  tgioolem 7866  lmuni 7902  lmle 7911  cmsss 7947  bcthlem7 7955  bcthlem9 7957  bcthlem13 7961  bcthlem14 7962  bcthlem15 7963  bcthlem16 7964  bcthlem18 7966  bcthlem19 7967  bcthlem20 7968  vcoprnelem 8149  cnnv 8258  nvelbl 8276  nvcnpi4 8368  nmlnogt0 8402  nmblolbii 8403  blocnilem 8408  ajmoi 8463  ubthlem10 8482  pilem1 8609  sinq12gt0t 8644  efifolem7 8662  efif1lem1 8664  shftefif1olem 8680  eff1i 8683  effoi 8684  hhnv 8971  norm1t 9060  hhssnv 9073  pjthlem10 9166  pjspansnt 9440  spanunsn 9442  fh1t 9501  fh2t 9502  cm2jt 9503  pjidt 9580  adjmo 9698  eleigvecclt 9822  eigvalclt 9824  eigvect 9825  eighmret 9826  eighmortht 9827  nmop0h 9854  nmbdoplb 9887  nmcopexlem5 9893  nmcoplb 9896  nmophm 9899  lnopcon 9901  lncnopbd 9904  nmbdfnlb 9916  nmcfnexlem5 9922  nmcfnlb 9925  lnfncon 9928  cnlnadjeu 9948  branmfnt 9976  rnbra 9978  nmopleidt 10010  strlem5 10120  hstrlem5 10128  dmdbr3 10170  dmdbr4 10171  mdsl3t 10180  hatomistic 10226  cvexchlem 10232  irredlem1 10254  irredlem2 10255  irred 10258  atcvat3 10260  atcvat4 10261  atabs 10265  mdsymlem1 10267  mdsymlem3 10269  mdsymlem5 10271  dmdbr5at 10284  cdj1 10294  uninqs 10378  cdrci 10417  hmeomap 10441  hmeocna 10442  hmeocnb 10443  fipfil2 10475  neifil 10478  mslb1 10509  ehm 10599  dehm 10600  cehm 10601

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