Theorem baibd 539

Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)

Hypothesis

Ref	Expression
baibd.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
baibd	⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

Proof of Theorem baibd

Step	Hyp	Ref	Expression
1		baibd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2		ibar 528	. . 3 ⊢ (𝜒 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
3	2	bicomd 223	. 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃))
4	1, 3	sylan9bb 509	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  rbaibd  540  pw2f1olem  9084  eluz  12858  elicc4  13420  s111  14620  limsupgle  15480  lo1resb  15567  o1resb  15569  isercolllem2  15669  divalgmodcl  16411  ismri2  17629  acsfiel2  17652  eqglact  19147  eqgid  19148  cntzel  19291  dprdsubg  19992  subgdmdprd  20002  dprd2da  20010  dmdprdpr  20017  issubrg3  20545  ishil2  21664  obslbs  21675  iscld2  22951  isperf3  23076  cncnp2  23204  cnnei  23205  trfbas2  23766  flimrest  23906  flfnei  23914  fclsrest  23947  tsmssubm  24066  isnghm2  24648  isnghm3  24649  isnmhm2  24676  iscfil2  25203  caucfil  25220  ellimc2  25815  cnlimc  25826  lhop1  25956  dvfsumlem1  25969  fsumharmonic  26958  fsumvma  27160  fsumvma2  27161  vmasum  27163  chpchtsum  27166  chpub  27167  rpvmasum2  27459  dchrisum0lem1  27463  dirith  27476  uvtx2vtx1edg  29309  uvtx2vtx1edgb  29310  iscplgrnb  29327  frgr3v  30188  adjeu  31802  suppiniseg  32596  suppss3  32636  nndiffz1  32697  indpreima  32760  islinds5  33300  fsumcvg4  33889  qqhval2lem  33920  eulerpartlemf  34310  elorvc  34400  hashreprin  34573  neibastop3  36301  relowlpssretop  37303  sstotbnd2  37719  isbnd3b  37730  lshpkr  39056  isat2  39226  islln4  39447  islpln4  39471  islvol4  39514  islhp2  39937  pw2f1o2val2  42989  modelaxreplem3  44932  rfcnpre1  44970  rfcnpre2  44982  joindm3  48822  meetdm3  48824  catprsc  48867