Theorem imbitrrid 156

Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) (Revised by NM, 22-Sep-2013.)

Hypotheses

Ref	Expression
imbitrrid.1	⊢ (𝜑 → 𝜃)
imbitrrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
imbitrrid	⊢ (𝜒 → (𝜑 → 𝜓))

Proof of Theorem imbitrrid

Step	Hyp	Ref	Expression
1		imbitrrid.1	. 2 ⊢ (𝜑 → 𝜃)
2		imbitrrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	bicomd 141	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	imbitrid 154	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl5ibrcom  157  biimprd  158  nbn2  705  anifpdc  995  limelon  4525  eldifpw  4603  ssonuni  4615  onsucuni2  4691  peano2  4722  limom  4741  elrnmpt1  5013  cnveqb  5223  cnveq0  5224  relcoi1  5299  f1ssf1  5651  ndmfvg  5706  ffvresb  5845  caovord3d  6233  poxp  6441  nnm0r  6725  nnacl  6726  nnacom  6730  nnaass  6731  nndi  6732  nnmass  6733  nnmsucr  6734  nnmcom  6735  brecop  6872  ecopovtrn  6879  ecopovtrng  6882  elpm2r  6913  map0g  6935  fundmen  7060  dom1o  7082  mapxpen  7114  mapunen  7117  phpm  7133  f1vrnfibi  7225  elfir  7273  mulcmpblnq  7699  ordpipqqs  7705  mulcmpblnq0  7775  genpprecll  7845  genppreclu  7846  addcmpblnr  8070  ax1rid  8208  axpre-mulgt0  8218  cnegexlem1  8465  msqge0  8908  mulge0  8911  ltleap  8924  nnmulcl  9278  nnsub  9296  elnn0z  9610  ztri3or0  9639  nneoor  9701  uz11  9898  xltnegi  10190  frec2uzuzd  10791  seq3fveq2  10864  seqfveq2g  10866  seq3shft2  10870  seqshft2g  10871  seq3split  10877  seqsplitg  10878  seq3caopr3  10880  seqcaopr3g  10881  seqf1oglem2a  10907  seq3id2  10915  seq3homo  10916  seqhomog  10919  m1expcl2  10950  expadd  10970  expmul  10973  faclbnd  11131  hashfzp1  11217  hashmap  11220  hashfacen  11236  seq3coll  11242  wrdsymb0  11285  len0nnbi  11287  wrd2ind  11443  pfxccatin12lem2c  11450  pfxccatin12lem2  11451  swrdccatin1d  11463  caucvgrelemcau  11694  recan  11823  rexanre  11934  fsumiun  12192  efexp  12397  dvdstr  12543  alzdvds  12569  zob  12606  bitsinv1  12677  gcdmultiplez  12746  dvdssq  12756  cncongr2  12830  prmdiveq  12962  pythagtriplem2  12993  pcexp  13036  elrestr  13548  ptex  13565  xpsff1o  13617  dfgrp3me  13859  mulgneg2  13913  mulgnnass  13914  mhmmulg  13920  rngpropd  14198  ringadd2  14274  mulgass2  14305  opprrngbg  14325  opprsubrngg  14461  subrngpropd  14466  subrgpropd  14503  rhmpropd  14504  lmodprop2d  14626  cnfldmulg  14854  cnfldexp  14855  restopn2  15178  txcn  15270  txlm  15274  isxms2  15447  rpcxpmul2  15908  gausslemma2dlem0i  16060  incistruhgr  16215  upgredg2vtx  16273  upgredgpr  16274  uhgr2edg  16331  wlkres  16504  clwwlknonex2  16564  eupth2lem3lem6fi  16596  bj-om  16847  bj-inf2vnlem2  16881  bj-inf2vn  16884  bj-inf2vn2  16885