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  4502  eldifpw  4580  ssonuni  4592  onsucuni2  4668  peano2  4699  limom  4718  elrnmpt1  4989  cnveqb  5199  cnveq0  5200  relcoi1  5275  f1ssf1  5624  ndmfvg  5679  ffvresb  5818  caovord3d  6203  poxp  6406  nnm0r  6690  nnacl  6691  nnacom  6695  nnaass  6696  nndi  6697  nnmass  6698  nnmsucr  6699  nnmcom  6700  brecop  6837  ecopovtrn  6844  ecopovtrng  6847  elpm2r  6878  map0g  6900  fundmen  7024  dom1o  7045  mapxpen  7077  phpm  7095  f1vrnfibi  7187  elfir  7215  mulcmpblnq  7631  ordpipqqs  7637  mulcmpblnq0  7707  genpprecll  7777  genppreclu  7778  addcmpblnr  8002  ax1rid  8140  axpre-mulgt0  8150  cnegexlem1  8397  msqge0  8839  mulge0  8842  ltleap  8855  nnmulcl  9207  nnsub  9225  elnn0z  9535  ztri3or0  9564  nneoor  9625  uz11  9822  xltnegi  10113  frec2uzuzd  10708  seq3fveq2  10781  seqfveq2g  10783  seq3shft2  10787  seqshft2g  10788  seq3split  10794  seqsplitg  10795  seq3caopr3  10797  seqcaopr3g  10798  seqf1oglem2a  10824  seq3id2  10832  seq3homo  10833  seqhomog  10836  m1expcl2  10867  expadd  10887  expmul  10890  faclbnd  11047  hashfzp1  11132  hashfacen  11144  seq3coll  11150  wrdsymb0  11193  len0nnbi  11195  wrd2ind  11351  pfxccatin12lem2c  11358  pfxccatin12lem2  11359  swrdccatin1d  11371  caucvgrelemcau  11601  recan  11730  rexanre  11841  fsumiun  12099  efexp  12304  dvdstr  12450  alzdvds  12476  zob  12513  bitsinv1  12584  gcdmultiplez  12653  dvdssq  12663  cncongr2  12737  prmdiveq  12869  pythagtriplem2  12900  pcexp  12943  elrestr  13391  ptex  13408  xpsff1o  13493  dfgrp3me  13744  mulgneg2  13804  mulgnnass  13805  mhmmulg  13811  rngpropd  14030  ringadd2  14102  mulgass2  14133  opprrngbg  14153  opprsubrngg  14287  subrngpropd  14292  subrgpropd  14329  rhmpropd  14330  lmodprop2d  14424  cnfldmulg  14652  cnfldexp  14653  restopn2  14974  txcn  15066  txlm  15070  isxms2  15243  rpcxpmul2  15704  gausslemma2dlem0i  15856  incistruhgr  16011  upgredg2vtx  16069  upgredgpr  16070  uhgr2edg  16127  wlkres  16300  clwwlknonex2  16360  eupth2lem3lem6fi  16392  bj-om  16633  bj-inf2vnlem2  16667  bj-inf2vn  16670  bj-inf2vn2  16671