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 676  biimp3a 919  sb5rf 1259  euor 1398  cgsexg 1831  cgsex2g 1832  cgsex4g 1833  ceqsex 1834  sbciegft 1959  ifboth 2375  elpwunsn 2912  limsssuc 3121  opelxp1 3205  relop 3275  resiexg 3396  fnbr 3590  f1o00 3714  tz7.44lem1 3927  oev2 4162  oesuc 4166  oecl 4172  omordi 4197  omwordri 4203  omword2 4205  omordlim 4208  omlimcl 4209  oeordi 4214  oewordri 4219  oelim2 4222  en3d 4401  pw2en 4446  fodomr 4483  mapunen 4502  onomeneq 4519  r1ord 4655  rankr1 4674  alephfp 4900  cfeq0 4914  nlt1pi 5033  indpi 5034  ltrpq 5085  addgt0sr 5213  cnegext 5348  leltnet 5521  xrleltnet 5558  addge0 5599  ne0gt0t 5619  muln0t 5698  divdivdivt 5785  ltmul12it 5841  recgt1it 5900  nn2get 5942  supxr 6081  supxr2 6082  flge0nn0t 6242  flge1nnt 6243  seq1m1 6319  eluzp1m1t 6433  eluzaddi 6436  eluzsubi 6437  elfzuz2t 6486  fsequb2 6524  expsubt 6598  expordit 6600  expord2t 6604  exple1t 6607  expubndt 6608  sqlecant 6641  bernneq 6652  bernneq2 6653  expnbndt 6654  absmaxt 6897  cvg2 6922  facwordit 6944  faclbnd4lem4 6951  bcval4t 6961  fsumsplit 7020  fsumrev 7029  fsumshft 7031  fsumcmpndx2 7042  fsumabs 7043  clm4le 7081  clm0i 7089  climge0 7112  climmullem1 7120  climmullem3 7122  climmullem4 7123  iserzex 7146  caucvg 7163  serzf0 7169  ser1f0 7170  ser1cmp 7174  ser1cmp2 7177  reccnv 7218  efcltlem1 7304  sin02gt0 7478  unbenlem 7504  elcls 7704  clsndisj 7706  unnei 7735  neissex 7738  metxptval 7830  metxpfval 7831  blss 7853  ssblex 7856  metcn 7889  metcnpi3 7892  metcnpi4 7893  metcni2 7895  tgioolem 7914  lmuni 7951  lmle 7960  cmsss 7997  bcthlem7 8005  bcthlem9 8007  bcthlem13 8011  bcthlem14 8012  bcthlem15 8013  bcthlem16 8014  bcthlem18 8016  bcthlem19 8017  bcthlem20 8018  vcoprnelem 8197  cnnv 8307  nvelbl 8325  nvcnpf 8328  nvcnpi3 8422  nvcnpi4 8423  nmlnogt0 8457  nmblolbii 8459  blocnilem 8464  ajmoi 8519  ubthlem10 8538  pilem1 8671  sinq12gt0t 8708  sineq0 8713  efifolem7 8728  efif1lem1 8730  shftefif1olem 8741  eff1i 8744  effoi 8745  hhnv 9032  norm1t 9121  hhssnv 9134  pjthlem10 9228  pjspansnt 9500  spanunsn 9502  fh1t 9561  fh2t 9562  cm2jt 9563  pjidt 9640  adjmo 9758  eleigvecclt 9883  eigvalclt 9885  eigvect 9886  eighmret 9887  eighmortht 9888  nmop0h 9916  nmbdoplb 9949  nmcopexlem5 9955  nmcoplb 9958  nmophm 9961  lnopcon 9963  lncnopbd 9966  nmbdfnlb 9978  nmcfnexlem5 9984  nmcfnlb 9987  lnfncon 9990  cnlnadjeu 10010  branmfnt 10038  rnbra 10040  nmopleidt 10072  strlem5 10182  hstrlem5 10190  dmdbr3 10232  dmdbr4 10233  mdsl3t 10243  hatomistic 10289  cvexchlem 10295  irredlem1 10317  irredlem2 10318  irred 10321  atcvat3 10323  atcvat4 10324  atabs 10328  mdsymlem1 10330  mdsymlem3 10332  mdsymlem5 10334  dmdbr5at 10349  cdj1 10360  uninqs 10441  cdrci 10494  hmeomap 10518  hmeocna 10519  hmeocnb 10520  fipfil2 10564  fipfil2OLD 10565  neifil 10568  mslb1 10629  ehm 10719  dehm 10720  cehm 10721

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