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  8464  msqge0  8907  mulge0  8910  ltleap  8923  nnmulcl  9275  nnsub  9293  elnn0z  9607  ztri3or0  9636  nneoor  9698  uz11  9895  xltnegi  10187  frec2uzuzd  10788  seq3fveq2  10861  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seqcaopr3g  10878  seqf1oglem2a  10904  seq3id2  10912  seq3homo  10913  seqhomog  10916  m1expcl2  10947  expadd  10967  expmul  10970  faclbnd  11128  hashfzp1  11214  hashmap  11217  hashfacen  11233  seq3coll  11239  wrdsymb0  11282  len0nnbi  11284  wrd2ind  11440  pfxccatin12lem2c  11447  pfxccatin12lem2  11448  swrdccatin1d  11460  caucvgrelemcau  11690  recan  11819  rexanre  11930  fsumiun  12188  efexp  12393  dvdstr  12539  alzdvds  12565  zob  12602  bitsinv1  12673  gcdmultiplez  12742  dvdssq  12752  cncongr2  12826  prmdiveq  12958  pythagtriplem2  12989  pcexp  13032  elrestr  13544  ptex  13561  xpsff1o  13646  dfgrp3me  13897  mulgneg2  13957  mulgnnass  13958  mhmmulg  13964  rngpropd  14183  ringadd2  14255  mulgass2  14286  opprrngbg  14306  opprsubrngg  14442  subrngpropd  14447  subrgpropd  14484  rhmpropd  14485  lmodprop2d  14608  cnfldmulg  14836  cnfldexp  14837  restopn2  15160  txcn  15252  txlm  15256  isxms2  15429  rpcxpmul2  15890  gausslemma2dlem0i  16042  incistruhgr  16197  upgredg2vtx  16255  upgredgpr  16256  uhgr2edg  16313  wlkres  16486  clwwlknonex2  16546  eupth2lem3lem6fi  16578  bj-om  16819  bj-inf2vnlem2  16853  bj-inf2vn  16856  bj-inf2vn2  16857