Theorem bi2anan9 694

Description: Deduction joining two equivalences to form equivalence of conjunctions.

Hypotheses

Ref	Expression
bi2an9.1	|- (ph -> (ps <-> ch))
bi2an9.2	|- (th -> (ta <-> et))

Assertion

Ref	Expression
bi2anan9	|- ((ph /\ th) -> ((ps /\ ta) <-> (ch /\ et)))

Proof of Theorem bi2anan9

Step	Hyp	Ref	Expression
1		bi2an9.1	. . 3 |- (ph -> (ps <-> ch))
2	1	anbi1d 679	. 2 |- (ph -> ((ps /\ ta) <-> (ch /\ ta)))
3		bi2an9.2	. . 3 |- (th -> (ta <-> et))
4	3	anbi2d 678	. 2 |- (th -> ((ch /\ ta) <-> (ch /\ et)))
5	2, 4	sylan9bb 599	1 |- ((ph /\ th) -> ((ps /\ ta) <-> (ch /\ et)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  bi2anan9r 695  2mo 1851  2eu6 1858  ralprg 3078  prssg 3140  iinxprg 3326  copsex4g 3540  opelxp 4036  eqrel 4077  eqrelrel 4085  feq23OLD 4555  dff13 4850  oprabval4g 4960  oprabval4gALT 4961  dfoprab5sf 5058  om00el 5255  oeoe 5274  th3qlem1 5373  th3qlem2 5374  oprec 5377  unen 5493  endisj 5496  aceq5lem4 5900  ordpipq 6208  genpv 6254  genpprecl 6256  distrlem5pr 6283  ltsrpr 6338  axcnre 6439  axmulgt0 6675  lt2msqi 7064  addltmul 7229  acdc3 8755  acdc2 8759  acdc5 8762  acdc 8764  ruclem12 8790  spwpr2 10001  uptx 10226  bra11 11679  leopadd 11703  bnj135 12467  fseq1cl 13619  dvds2lem 13667  gcddvds 13722  dvdsgcd 13765  altopelaltxp 14099  int2pre 14578  rcfpfillem4 14931  filnetlem4 15643  filnet 15645  resoprab2 15710  fzadd2 15791  txsubsp 15912  txcld 15914  cnoproprabco 15919  txmet 15925  bfplem3 16000  joinval2 16816  meetval2 16823

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 164  df-an 242

Copyright terms: Public domain