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  4494  eldifpw  4572  ssonuni  4584  onsucuni2  4660  peano2  4691  limom  4710  elrnmpt1  4981  cnveqb  5190  cnveq0  5191  relcoi1  5266  ndmfvg  5666  ffvresb  5806  caovord3d  6188  poxp  6392  nnm0r  6642  nnacl  6643  nnacom  6647  nnaass  6648  nndi  6649  nnmass  6650  nnmsucr  6651  nnmcom  6652  brecop  6789  ecopovtrn  6796  ecopovtrng  6799  elpm2r  6830  map0g  6852  fundmen  6976  dom1o  6997  mapxpen  7029  phpm  7047  f1vrnfibi  7138  elfir  7166  mulcmpblnq  7581  ordpipqqs  7587  mulcmpblnq0  7657  genpprecll  7727  genppreclu  7728  addcmpblnr  7952  ax1rid  8090  axpre-mulgt0  8100  cnegexlem1  8347  msqge0  8789  mulge0  8792  ltleap  8805  nnmulcl  9157  nnsub  9175  elnn0z  9485  ztri3or0  9514  nneoor  9575  uz11  9772  xltnegi  10063  frec2uzuzd  10657  seq3fveq2  10730  seqfveq2g  10732  seq3shft2  10736  seqshft2g  10737  seq3split  10743  seqsplitg  10744  seq3caopr3  10746  seqcaopr3g  10747  seqf1oglem2a  10773  seq3id2  10781  seq3homo  10782  seqhomog  10785  m1expcl2  10816  expadd  10836  expmul  10839  faclbnd  10996  hashfzp1  11081  hashfacen  11093  seq3coll  11099  wrdsymb0  11139  len0nnbi  11141  wrd2ind  11297  pfxccatin12lem2c  11304  pfxccatin12lem2  11305  swrdccatin1d  11317  caucvgrelemcau  11534  recan  11663  rexanre  11774  fsumiun  12031  efexp  12236  dvdstr  12382  alzdvds  12408  zob  12445  bitsinv1  12516  gcdmultiplez  12585  dvdssq  12595  cncongr2  12669  prmdiveq  12801  pythagtriplem2  12832  pcexp  12875  elrestr  13323  ptex  13340  xpsff1o  13425  dfgrp3me  13676  mulgneg2  13736  mulgnnass  13737  mhmmulg  13743  rngpropd  13961  ringadd2  14033  mulgass2  14064  opprrngbg  14084  opprsubrngg  14218  subrngpropd  14223  subrgpropd  14260  rhmpropd  14261  lmodprop2d  14355  cnfldmulg  14583  cnfldexp  14584  restopn2  14900  txcn  14992  txlm  14996  isxms2  15169  rpcxpmul2  15630  gausslemma2dlem0i  15779  incistruhgr  15934  upgredg2vtx  15992  upgredgpr  15993  uhgr2edg  16050  wlkres  16188  clwwlknonex2  16248  bj-om  16482  bj-inf2vnlem2  16516  bj-inf2vn  16519  bj-inf2vn2  16520