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  9114  eluz  12889  elicc4  13450  s111  14649  limsupgle  15509  lo1resb  15596  o1resb  15598  isercolllem2  15698  divalgmodcl  16440  ismri2  17676  acsfiel2  17699  eqglact  19209  eqgid  19210  cntzel  19353  dprdsubg  20058  subgdmdprd  20068  dprd2da  20076  dmdprdpr  20083  issubrg3  20616  ishil2  21756  obslbs  21767  iscld2  23051  isperf3  23176  cncnp2  23304  cnnei  23305  trfbas2  23866  flimrest  24006  flfnei  24014  fclsrest  24047  tsmssubm  24166  isnghm2  24760  isnghm3  24761  isnmhm2  24788  iscfil2  25313  caucfil  25330  ellimc2  25926  cnlimc  25937  lhop1  26067  dvfsumlem1  26080  fsumharmonic  27069  fsumvma  27271  fsumvma2  27272  vmasum  27274  chpchtsum  27277  chpub  27278  rpvmasum2  27570  dchrisum0lem1  27574  dirith  27587  uvtx2vtx1edg  29429  uvtx2vtx1edgb  29430  iscplgrnb  29447  frgr3v  30303  adjeu  31917  suppiniseg  32700  suppss3  32741  nndiffz1  32794  islinds5  33374  fsumcvg4  33910  qqhval2lem  33943  indpreima  34005  eulerpartlemf  34351  elorvc  34440  hashreprin  34613  neibastop3  36344  relowlpssretop  37346  sstotbnd2  37760  isbnd3b  37771  lshpkr  39098  isat2  39268  islln4  39489  islpln4  39513  islvol4  39556  islhp2  39979  pw2f1o2val2  43028  modelaxreplem3  44944  rfcnpre1  44956  rfcnpre2  44968  joindm3  48765  meetdm3  48767  catprsc  48801