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  709  anifpdc  999  limelon  4542  eldifpw  4621  ssonuni  4633  onsucuni2  4709  peano2  4740  limom  4759  elrnmpt1  5031  cnveqb  5241  cnveq0  5242  relcoi1  5317  f1ssf1  5669  ndmfvg  5724  ffvresb  5865  caovord3d  6254  poxp  6462  nnm0r  6746  nnacl  6747  nnacom  6751  nnaass  6752  nndi  6753  nnmass  6754  nnmsucr  6755  nnmcom  6756  brecop  6893  ecopovtrn  6900  ecopovtrng  6903  elpm2r  6934  map0g  6963  fundmen  7088  dom1o  7110  mapxpen  7142  mapunen  7145  phpm  7161  f1vrnfibi  7253  elfir  7301  mulcmpblnq  7729  ordpipqqs  7735  mulcmpblnq0  7805  genpprecll  7875  genppreclu  7876  addcmpblnr  8100  ax1rid  8238  axpre-mulgt0  8248  cnegexlem1  8495  msqge0  8938  mulge0  8941  ltleap  8954  nnmulcl  9308  nnsub  9326  elnn0z  9640  ztri3or0  9669  nneoor  9731  uz11  9928  xltnegi  10220  frec2uzuzd  10822  seq3fveq2  10895  seqfveq2g  10897  seq3shft2  10901  seqshft2g  10902  seq3split  10908  seqsplitg  10909  seq3caopr3  10911  seqcaopr3g  10912  seqf1oglem2a  10938  seq3id2  10946  seq3homo  10947  seqhomog  10950  m1expcl2  10981  expadd  11001  expmul  11004  faclbnd  11162  hashfzp1  11248  hashmap  11251  hashfacen  11267  hashf1lem2  11269  hashf1  11270  seq3coll  11277  wrdsymb0  11320  len0nnbi  11322  wrd2ind  11478  pfxccatin12lem2c  11485  pfxccatin12lem2  11486  swrdccatin1d  11498  caucvgrelemcau  11729  recan  11858  rexanre  11969  fsumiun  12227  efexp  12432  dvdstr  12578  alzdvds  12604  zob  12641  bitsinv1  12712  gcdmultiplez  12781  dvdssq  12791  cncongr2  12865  prmdiveq  12997  pythagtriplem2  13028  pcexp  13071  elrestr  13584  ptex  13601  xpsff1o  13653  dfgrp3me  13888  mulgneg2  13942  mulgnnass  13943  mhmmulg  13949  rngpropd  14237  ringadd2  14315  mulgass2  14346  opprrngbg  14366  opprsubrngg  14502  subrngpropd  14507  subrgpropd  14544  rhmpropd  14545  lmodprop2d  14668  cnfldmulg  14896  cnfldexp  14897  assapropd  14997  restopn2  15267  txcn  15359  txlm  15363  isxms2  15536  rpcxpmul2  15998  gausslemma2dlem0i  16159  incistruhgr  16314  upgredg2vtx  16372  upgredgpr  16373  uhgr2edg  16430  wlkres  16603  clwwlknonex2  16663  eupth2lem3lem6fi  16695  bj-om  16946  bj-inf2vnlem2  16980  bj-inf2vn  16983  bj-inf2vn2  16984