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  698  limelon  4434  eldifpw  4512  ssonuni  4524  onsucuni2  4600  peano2  4631  limom  4650  elrnmpt1  4917  cnveqb  5125  cnveq0  5126  relcoi1  5201  ndmfvg  5589  ffvresb  5725  caovord3d  6094  poxp  6290  nnm0r  6537  nnacl  6538  nnacom  6542  nnaass  6543  nndi  6544  nnmass  6545  nnmsucr  6546  nnmcom  6547  brecop  6684  ecopovtrn  6691  ecopovtrng  6694  elpm2r  6725  map0g  6747  fundmen  6865  mapxpen  6909  phpm  6926  f1vrnfibi  7011  elfir  7039  mulcmpblnq  7435  ordpipqqs  7441  mulcmpblnq0  7511  genpprecll  7581  genppreclu  7582  addcmpblnr  7806  ax1rid  7944  axpre-mulgt0  7954  cnegexlem1  8201  msqge0  8643  mulge0  8646  ltleap  8659  nnmulcl  9011  nnsub  9029  elnn0z  9339  ztri3or0  9368  nneoor  9428  uz11  9624  xltnegi  9910  frec2uzuzd  10494  seq3fveq2  10567  seqfveq2g  10569  seq3shft2  10573  seqshft2g  10574  seq3split  10580  seqsplitg  10581  seq3caopr3  10583  seqcaopr3g  10584  seqf1oglem2a  10610  seq3id2  10618  seq3homo  10619  seqhomog  10622  m1expcl2  10653  expadd  10673  expmul  10676  faclbnd  10833  hashfzp1  10916  hashfacen  10928  seq3coll  10934  wrdsymb0  10967  len0nnbi  10969  caucvgrelemcau  11145  recan  11274  rexanre  11385  fsumiun  11642  efexp  11847  dvdstr  11993  alzdvds  12019  zob  12056  gcdmultiplez  12188  dvdssq  12198  cncongr2  12272  prmdiveq  12404  pythagtriplem2  12435  pcexp  12478  elrestr  12918  ptex  12935  xpsff1o  12992  dfgrp3me  13232  mulgneg2  13286  mulgnnass  13287  mhmmulg  13293  rngpropd  13511  ringadd2  13583  mulgass2  13614  opprrngbg  13634  opprsubrngg  13767  subrngpropd  13772  subrgpropd  13809  rhmpropd  13810  lmodprop2d  13904  cnfldmulg  14132  cnfldexp  14133  restopn2  14419  txcn  14511  txlm  14515  isxms2  14688  rpcxpmul2  15149  gausslemma2dlem0i  15298  bj-om  15583  bj-inf2vnlem2  15617  bj-inf2vn  15620  bj-inf2vn2  15621