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  702  anifpdc  992  limelon  4490  eldifpw  4568  ssonuni  4580  onsucuni2  4656  peano2  4687  limom  4706  elrnmpt1  4975  cnveqb  5184  cnveq0  5185  relcoi1  5260  ndmfvg  5660  ffvresb  5800  caovord3d  6182  poxp  6384  nnm0r  6633  nnacl  6634  nnacom  6638  nnaass  6639  nndi  6640  nnmass  6641  nnmsucr  6642  nnmcom  6643  brecop  6780  ecopovtrn  6787  ecopovtrng  6790  elpm2r  6821  map0g  6843  fundmen  6967  dom1o  6985  mapxpen  7017  phpm  7035  f1vrnfibi  7120  elfir  7148  mulcmpblnq  7563  ordpipqqs  7569  mulcmpblnq0  7639  genpprecll  7709  genppreclu  7710  addcmpblnr  7934  ax1rid  8072  axpre-mulgt0  8082  cnegexlem1  8329  msqge0  8771  mulge0  8774  ltleap  8787  nnmulcl  9139  nnsub  9157  elnn0z  9467  ztri3or0  9496  nneoor  9557  uz11  9753  xltnegi  10039  frec2uzuzd  10632  seq3fveq2  10705  seqfveq2g  10707  seq3shft2  10711  seqshft2g  10712  seq3split  10718  seqsplitg  10719  seq3caopr3  10721  seqcaopr3g  10722  seqf1oglem2a  10748  seq3id2  10756  seq3homo  10757  seqhomog  10760  m1expcl2  10791  expadd  10811  expmul  10814  faclbnd  10971  hashfzp1  11054  hashfacen  11066  seq3coll  11072  wrdsymb0  11112  len0nnbi  11114  wrd2ind  11263  pfxccatin12lem2c  11270  pfxccatin12lem2  11271  swrdccatin1d  11283  caucvgrelemcau  11499  recan  11628  rexanre  11739  fsumiun  11996  efexp  12201  dvdstr  12347  alzdvds  12373  zob  12410  bitsinv1  12481  gcdmultiplez  12550  dvdssq  12560  cncongr2  12634  prmdiveq  12766  pythagtriplem2  12797  pcexp  12840  elrestr  13288  ptex  13305  xpsff1o  13390  dfgrp3me  13641  mulgneg2  13701  mulgnnass  13702  mhmmulg  13708  rngpropd  13926  ringadd2  13998  mulgass2  14029  opprrngbg  14049  opprsubrngg  14183  subrngpropd  14188  subrgpropd  14225  rhmpropd  14226  lmodprop2d  14320  cnfldmulg  14548  cnfldexp  14549  restopn2  14865  txcn  14957  txlm  14961  isxms2  15134  rpcxpmul2  15595  gausslemma2dlem0i  15744  incistruhgr  15898  upgredg2vtx  15954  upgredgpr  15955  uhgr2edg  16012  wlkres  16098  bj-om  16324  bj-inf2vnlem2  16358  bj-inf2vn  16361  bj-inf2vn2  16362